--- a/doc-src/TutorialI/document/appendix0.tex Tue Aug 28 18:46:15 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,190 +0,0 @@
-\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}