--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Tutorial/document/appendix0.tex Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,190 @@
+\appendix
+
+\chapter{Appendix}
+\label{sec:Appendix}
+
+\begin{table}[htbp]
+\begin{center}
+\begin{tabular}{|l|l|l|}
+\hline
+\indexboldpos{\isasymlbrakk}{$Isabrl} &
+\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
+\verb$\<lbrakk>$ \\
+\indexboldpos{\isasymrbrakk}{$Isabrr} &
+\texttt{|]}\index{$Isabrr@\ttrbr|bold} &
+\verb$\<rbrakk>$ \\
+\indexboldpos{\isasymImp}{$IsaImp} &
+\ttindexboldpos{==>}{$IsaImp} &
+\verb$\<Longrightarrow>$ \\
+\isasymAnd\index{$IsaAnd@\isasymAnd|bold}&
+\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
+\verb$\<And>$ \\
+\indexboldpos{\isasymequiv}{$IsaEq} &
+\ttindexboldpos{==}{$IsaEq} &
+\verb$\<equiv>$ \\
+\indexboldpos{\isasymrightleftharpoons}{$IsaEqTrans} &
+\ttindexboldpos{==}{$IsaEq} &
+\verb$\<rightleftharpoons>$ \\
+\indexboldpos{\isasymrightharpoonup}{$IsaEqTrans1} &
+\ttindexboldpos{=>}{$IsaFun} &
+\verb$\<rightharpoonup>$ \\
+\indexboldpos{\isasymleftharpoondown}{$IsaEqTrans2} &
+\ttindexboldpos{<=}{$IsaFun2} &
+\verb$\<leftharpoondown>$ \\
+\indexboldpos{\isasymlambda}{$Isalam} &
+\texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
+\verb$\<lambda>$ \\
+\indexboldpos{\isasymFun}{$IsaFun} &
+\ttindexboldpos{=>}{$IsaFun} &
+\verb$\<Rightarrow>$ \\
+\indexboldpos{\isasymand}{$HOL0and} &
+\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
+\verb$\<and>$ \\
+\indexboldpos{\isasymor}{$HOL0or} &
+\texttt{|}\index{$HOL0or@\ttor|bold} &
+\verb$\<or>$ \\
+\indexboldpos{\isasymimp}{$HOL0imp} &
+\ttindexboldpos{-->}{$HOL0imp} &
+\verb$\<longrightarrow>$ \\
+\indexboldpos{\isasymnot}{$HOL0not} &
+\verb$~$\index{$HOL0not@\verb$~$|bold} &
+\verb$\<not>$ \\
+\indexboldpos{\isasymnoteq}{$HOL0noteq} &
+\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
+\verb$\<noteq>$ \\
+\indexboldpos{\isasymforall}{$HOL0All} &
+\ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} &
+\verb$\<forall>$ \\
+\indexboldpos{\isasymexists}{$HOL0Ex} &
+\ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
+\verb$\<exists>$ \\
+\isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
+\ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
+\verb$\<exists>!$\\
+\indexboldpos{\isasymepsilon}{$HOL0ExSome} &
+\ttindexbold{SOME}, \isa{\at}\index{$HOL2list@\isa{\at}} &
+\verb$\<epsilon>$\\
+\indexboldpos{\isasymcirc}{$HOL1} &
+\ttindexbold{o} &
+\verb$\<circ>$\\
+\indexboldpos{\isasymbar~\isasymbar}{$HOL2arithfun}&
+\ttindexbold{abs}&
+\verb$\<bar> \<bar>$\\
+\indexboldpos{\isasymle}{$HOL2arithrel}&
+\isadxboldpos{<=}{$HOL2arithrel}&
+\verb$\<le>$\\
+\indexboldpos{\isasymtimes}{$Isatype}&
+\ttindexboldpos{*}{$HOL2arithfun} &
+\verb$\<times>$\\
+\indexboldpos{\isasymin}{$HOL3Set0a}&
+\ttindexboldpos{:}{$HOL3Set0b} &
+\verb$\<in>$\\
+\isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} &
+\verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} &
+\verb$\<notin>$\\
+\indexboldpos{\isasymsubseteq}{$HOL3Set0e}&
+\verb$<=$ & \verb$\<subseteq>$\\
+\indexboldpos{\isasymsubset}{$HOL3Set0f}&
+\verb$<$ & \verb$\<subset>$\\
+\indexboldpos{\isasymunion}{$HOL3Set1}&
+\ttindexbold{Un} &
+\verb$\<union>$\\
+\indexboldpos{\isasyminter}{$HOL3Set1}&
+\ttindexbold{Int} &
+\verb$\<inter>$\\
+\isasymUnion\index{$HOL3Set2@\isasymUnion|bold}&
+\ttindexbold{UN}, \ttindexbold{Union} &
+\verb$\<Union>$\\
+\isasymInter\index{$HOL3Set2@\isasymInter|bold}&
+\ttindexbold{INT}, \ttindexbold{Inter} &
+\verb$\<Inter>$\\
+\isactrlsup{\isacharasterisk}\index{$HOL4star@\isactrlsup{\isacharasterisk}|bold}&
+\verb$^*$\index{$HOL4star@\verb$^$\texttt{*}|bold} &
+\verb$\<^sup>*$\\
+\isasyminverse\index{$HOL4inv@\isasyminverse|bold}&
+\verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} &
+\verb$\<inverse>$\\
+\hline
+\end{tabular}
+\end{center}
+\caption{Mathematical Symbols, Their \textsc{ascii}-Equivalents and Internal Names}
+\label{tab:ascii}
+\end{table}\indexbold{ASCII@\textsc{ascii} symbols}
+
+\input{appendix.tex}
+
+\begin{table}[htbp]
+\begin{center}
+\begin{tabular}{@{}|lllllllll|@{}}
+\hline
+\texttt{ALL} &
+\texttt{BIT} &
+\texttt{CHR} &
+\texttt{EX} &
+\texttt{GREATEST} &
+\texttt{INT} &
+\texttt{Int} &
+\texttt{LEAST} &
+\texttt{O} \\
+\texttt{OFCLASS} &
+\texttt{PI} &
+\texttt{PROP} &
+\texttt{SIGMA} &
+\texttt{SOME} &
+\texttt{THE} &
+\texttt{TYPE} &
+\texttt{UN} &
+\texttt{Un} \\
+\texttt{WRT} &
+\texttt{case} &
+\texttt{choose} &
+\texttt{div} &
+\texttt{dvd} &
+\texttt{else} &
+\texttt{funcset} &
+\texttt{if} &
+\texttt{in} \\
+\texttt{let} &
+\texttt{mem} &
+\texttt{mod} &
+\texttt{o} &
+\texttt{of} &
+\texttt{op} &
+\texttt{then} &&\\
+\hline
+\end{tabular}
+\end{center}
+\caption{Reserved Words in HOL Terms}
+\label{tab:ReservedWords}
+\end{table}
+
+
+%\begin{table}[htbp]
+%\begin{center}
+%\begin{tabular}{|lllll|}
+%\hline
+%\texttt{and} &
+%\texttt{binder} &
+%\texttt{concl} &
+%\texttt{congs} \\
+%\texttt{distinct} &
+%\texttt{files} &
+%\texttt{in} &
+%\texttt{induction} &
+%\texttt{infixl} \\
+%\texttt{infixr} &
+%\texttt{inject} &
+%\texttt{intrs} &
+%\texttt{is} &
+%\texttt{monos} \\
+%\texttt{output} &
+%\texttt{where} &
+% &
+% &
+% \\
+%\hline
+%\end{tabular}
+%\end{center}
+%\caption{Minor Keywords in HOL Theories}
+%\label{tab:keywords}
+%\end{table}