started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
theory Appendix
imports Main
begin
text {* \appendix *}
chapter {* Recipes *}
text {*
Possible topics:
\begin{itemize}
\item translations/print translations;
@{ML "ProofContext.print_syntax"}
\item user space type systems (in the form that already exists)
\item unification and typing algorithms
(@{ML_file "Pure/pattern.ML"} implements HOPU)
\item useful datastructures: discrimination nets, association lists
\end{itemize}
*}
end