Matthews, S. (1996). Implementing $\textrm FS_0$ in Isabelle: Adding Structure at the Metalevel. In L. C., Paulson (Ed.), Design and Implementation of Symbolic Computation Systems (DISCO'96) (pp. 228-239). Berlin, Germany: Springer.