--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/appendix.tex Wed Apr 19 11:54:39 2000 +0200
@@ -0,0 +1,162 @@
+\appendix
+
+\chapter{Appendix}
+\label{sec:Appendix}
+
+\begin{figure}[htbp]
+\begin{center}
+\begin{tabular}{|ccccccccccc|}
+\hline
+\indexboldpos{\isasymand}{$HOL0and} &
+\indexboldpos{\isasymor}{$HOL0or} &
+\indexboldpos{\isasymimp}{$HOL0imp} &
+\indexboldpos{\isasymnot}{$HOL0not} &
+\indexboldpos{\isasymnoteq}{$HOL0noteq} &
+\indexboldpos{\isasymforall}{$HOL0All} &
+\isasymforall &
+\indexboldpos{\isasymexists}{$HOL0Ex} &
+\isasymexists &
+\isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
+\isasymuniqex \\
+\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
+\texttt{|}\index{$HOL0or@\ttor|bold} &
+\ttindexboldpos{-->}{$HOL0imp} &
+\verb$~$\index{$HOL0not@\verb$~$|bold} &
+\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
+\ttindexbold{ALL} &
+\texttt{!}\index{$HOL0All@\ttall|bold} &
+\ttindexbold{EX} &
+\texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
+\ttEXU\index{EXX@\ttEXU|bold} &
+\ttuniquex\index{$HOL0ExU@\ttuniquex|bold}\\
+\hline\hline
+\indexboldpos{\isasymlbrakk}{$Isabrl} &
+\indexboldpos{\isasymrbrakk}{$Isabrr} &
+\indexboldpos{\isasymImp}{$IsaImp} &
+\indexboldpos{\isasymAnd}{$IsaAnd} &
+\indexboldpos{\isasymequiv}{$IsaEq} &
+\indexboldpos{\isasymlambda}{$Isalam} &
+\indexboldpos{\isasymFun}{$IsaFun}&
+&
+&
+&
+\\
+\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
+\texttt{|]}\index{$Isabrr@\ttrbr|bold} &
+\ttindexboldpos{==>}{$IsaImp} &
+\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
+\ttindexboldpos{==}{$IsaEq} &
+\texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
+\ttindexboldpos{=>}{$IsaFun}&
+&
+&
+&
+ \\
+\hline\hline
+\indexboldpos{\isasymcirc}{$HOL1} &
+\indexboldpos{\isasymle}{$HOL2arithrel}&
+&
+&
+&
+&
+&
+&
+&
+&
+ \\
+\ttindexbold{o} &
+\ttindexboldpos{<=}{$HOL2arithrel}&
+&
+&
+&
+&
+&
+&
+&
+&
+\\
+\hline
+\end{tabular}
+\end{center}
+\caption{Mathematical symbols and their ASCII-equivalents}
+\label{fig:ascii}
+\end{figure}
+
+\begin{figure}[htbp]
+\begin{center}
+\begin{tabular}{|lllll|}
+\hline
+\texttt{and} &
+\texttt{arities} &
+\texttt{assumes} &
+\texttt{axclass} &
+\texttt{binder} \\
+\texttt{classes} &
+\texttt{constdefs} &
+\texttt{consts} &
+\texttt{default} &
+\texttt{defines} \\
+\texttt{defs} &
+\texttt{end} &
+\texttt{fixes} &
+\texttt{global} &
+\texttt{inductive} \\
+\texttt{infixl} &
+\texttt{infixr} &
+\texttt{instance} &
+\texttt{local} &
+\texttt{locale} \\
+\texttt{mixfix} &
+\texttt{ML} &
+\texttt{MLtext} &
+\texttt{nonterminals} &
+\texttt{oracle} \\
+\texttt{output} &
+\texttt{path} &
+\texttt{primrec} &
+\texttt{rules} &
+\texttt{setup} \\
+\texttt{syntax} &
+\texttt{translations} &
+\texttt{typedef} &
+\texttt{types} &\\
+\hline
+\end{tabular}
+\end{center}
+\caption{Keywords in theory files}
+\label{fig:keywords}
+\end{figure}
+
+\begin{figure}[htbp]
+\begin{center}
+\begin{tabular}{|lllll|}
+\hline
+\texttt{ALL} &
+\texttt{case} &
+\texttt{div} &
+\texttt{dvd} &
+\texttt{else} \\
+\texttt{EX} &
+\texttt{if} &
+\texttt{in} &
+\texttt{INT} &
+\texttt{Int} \\
+\texttt{LEAST} &
+\texttt{let} &
+\texttt{mod} &
+\texttt{O} &
+\texttt{o} \\
+\texttt{of} &
+\texttt{op} &
+\texttt{PROP} &
+\texttt{SIGMA} &
+\texttt{then} \\
+\texttt{Times} &
+\texttt{UN} &
+\texttt{Un} &&\\
+\hline
+\end{tabular}
+\end{center}
+\caption{Reserved words in HOL}
+\label{fig:ReservedWords}
+\end{figure}