, You can export the code of Isabelle/HOL functions into various programming languages (SML, Haskell, OCaml and Scala) using the export code directive. For instance, below all the function definitions and outside of a proof, you can type: export code remove numNodes subTree in Scala whose effect is to export all the necessary material for the above functions to run in Scala

, Many thanks to Tobias Nipkow, Jasmin Christian Blanchette and all the developers on Isabelle's mailing list. Many thanks also to Pauline Bolignano, Jørgen Villadsen and Yannick Zakowski for feedback on the tutorial