CookBook/Appendix.thy
changeset 170 90bee31628dc
parent 168 009ca4807baa
child 182 4d0e2edd476d
equal deleted inserted replaced
169:d3fcc1a0272c 170:90bee31628dc
     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   \begin{itemize}
       
    15   \item translations/print translations; 
       
    16   @{ML "ProofContext.print_syntax"}
    17   
    17   
    18   User Space Type Systems (in the already existing form)
    18   \item user space type systems (in the form that already exists)
       
    19 
       
    20   \item unification and typing algorithms
       
    21 
       
    22   \item useful datastructures: discrimination nets, association lists
       
    23   \end{itemize}
    19 *}
    24 *}
    20 
    25 
    21 end
    26 end
    22   
       
    23 
       
    24 
       
    25