+ −
theory Appendix+ −
imports Base+ −
begin+ −
+ −
(*<*)+ −
setup{*+ −
open_file_with_prelude + −
"Recipes_Code.thy"+ −
["theory Recipes", "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 useful datastructures: discrimination nets, graphs, association lists+ −
+ −
\item Brief history of Isabelle+ −
\end{itemize}+ −
*}+ −
+ −
end+ −