CookBook/Appendix.thy
author Christian Urban <urbanc@in.tum.de>
Sun, 08 Mar 2009 20:53:00 +0000
changeset 163 2319cff107f0
parent 162 3fb9f820a294
child 164 3f617d7a2691
permissions -rw-r--r--
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive


theory Appendix
imports Main
begin

text {* \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