1 

     2 theory Appendix

     3 imports Main

     4 begin

     5 

     6 

     7 text {* \appendix *}

     8 

     9 

    10 chapter {* Recipes *}

    11 

    12 text {*

    13   Possible topics: 

    14 

    15   \begin{itemize}

    16   \item translations/print translations; 

    17   @{ML "ProofContext.print_syntax"}

    18   

    19   \item user space type systems (in the form that already exists)

    20 

    21   \item unification and typing algorithms 

    22   (@{ML_file "Pure/pattern.ML"} implements HOPU)

    23 

    24   \item useful datastructures: discrimination nets, association lists

    25   \end{itemize}

    26 *}

    27 

    28 end