some additions to the simplifier section and general tuning
theory Appendiximports Mainbegintext {* \appendix *}chapter {* Recipes *}text {* Possible further topics: translations/print translations @{ML "ProofContext.print_syntax"} user space type systems (in the form that already exists) unification and typing algorithms*}end