Mutually Recursive Partial Functions.
René Thiemann · 2014
We provide a wrapper around the partial-function command which supports mutual recursion. Our results have been used to simplify the development of mutually recursive parsers, e.g., a parser to convert external proofs given in XML into some mutually recursive datatype within Isabelle/HOL.