CookBook/Appendix.thy
changeset 162 3fb9f820a294
parent 131 8db9195bb3e9
child 164 3f617d7a2691
equal deleted inserted replaced
161:83f36a1c62f2 162:3fb9f820a294
     3 imports Main
     3 imports Main
     4 begin
     4 begin
     5 
     5 
     6 text {* \appendix *}
     6 text {* \appendix *}
     7 
     7 
     8 text {*
       
     9   Possible topics: translations/print translations
       
    10 *}
       
    11 
       
    12 
     8 
    13 chapter {* Recipes *}
     9 chapter {* Recipes *}
    14 
    10 
    15 text {*
    11 text {*
    16   Possible topics: translations/print translations
    12   Possible further topics: 
       
    13 
       
    14   translations/print translations
       
    15 
       
    16   @{ML "ProofContext.print_syntax"}
    17   
    17   
    18   User Space Type Systems (in the already existing form)
    18   user space type systems (in the form that already exists)
       
    19 
       
    20   unification and typing algorithms
    19 *}
    21 *}
    20 
    22 
    21 end
    23 end
    22   
    24   
    23 
    25