added an antiquotation for printing the raw proof state; polished the example about proof state
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