1\appendix 2 3\chapter{Appendix} 4\label{sec:Appendix} 5 6\begin{table}[htbp] 7\begin{center} 8\begin{tabular}{|l|l|l|} 9\hline 10\indexboldpos{\isasymlbrakk}{$Isabrl} & 11\texttt{[|}\index{$Isabrl@\ttlbr|bold} & 12\verb$\<lbrakk>$ \\ 13\indexboldpos{\isasymrbrakk}{$Isabrr} & 14\texttt{|]}\index{$Isabrr@\ttrbr|bold} & 15\verb$\<rbrakk>$ \\ 16\indexboldpos{\isasymImp}{$IsaImp} & 17\ttindexboldpos{==>}{$IsaImp} & 18\verb$\<Longrightarrow>$ \\ 19\isasymAnd\index{$IsaAnd@\isasymAnd|bold}& 20\texttt{!!}\index{$IsaAnd@\ttAnd|bold} & 21\verb$\<And>$ \\ 22\indexboldpos{\isasymequiv}{$IsaEq} & 23\ttindexboldpos{==}{$IsaEq} & 24\verb$\<equiv>$ \\ 25\indexboldpos{\isasymrightleftharpoons}{$IsaEqTrans} & 26\ttindexboldpos{==}{$IsaEq} & 27\verb$\<rightleftharpoons>$ \\ 28\indexboldpos{\isasymrightharpoonup}{$IsaEqTrans1} & 29\ttindexboldpos{=>}{$IsaFun} & 30\verb$\<rightharpoonup>$ \\ 31\indexboldpos{\isasymleftharpoondown}{$IsaEqTrans2} & 32\ttindexboldpos{<=}{$IsaFun2} & 33\verb$\<leftharpoondown>$ \\ 34\indexboldpos{\isasymlambda}{$Isalam} & 35\texttt{\%}\indexbold{$Isalam@\texttt{\%}} & 36\verb$\<lambda>$ \\ 37\indexboldpos{\isasymFun}{$IsaFun} & 38\ttindexboldpos{=>}{$IsaFun} & 39\verb$\<Rightarrow>$ \\ 40\indexboldpos{\isasymand}{$HOL0and} & 41\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} & 42\verb$\<and>$ \\ 43\indexboldpos{\isasymor}{$HOL0or} & 44\texttt{|}\index{$HOL0or@\ttor|bold} & 45\verb$\<or>$ \\ 46\indexboldpos{\isasymimp}{$HOL0imp} & 47\ttindexboldpos{-->}{$HOL0imp} & 48\verb$\<longrightarrow>$ \\ 49\indexboldpos{\isasymnot}{$HOL0not} & 50\verb$~$\index{$HOL0not@\verb$~$|bold} & 51\verb$\<not>$ \\ 52\indexboldpos{\isasymnoteq}{$HOL0noteq} & 53\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} & 54\verb$\<noteq>$ \\ 55\indexboldpos{\isasymforall}{$HOL0All} & 56\ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} & 57\verb$\<forall>$ \\ 58\indexboldpos{\isasymexists}{$HOL0Ex} & 59\ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} & 60\verb$\<exists>$ \\ 61\isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} & 62\ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} & 63\verb$\<exists>!$\\ 64\indexboldpos{\isasymepsilon}{$HOL0ExSome} & 65\ttindexbold{SOME}, \isa{\at}\index{$HOL2list@\isa{\at}} & 66\verb$\<epsilon>$\\ 67\indexboldpos{\isasymcirc}{$HOL1} & 68\ttindexbold{o} & 69\verb$\<circ>$\\ 70\indexboldpos{\isasymbar~\isasymbar}{$HOL2arithfun}& 71\ttindexbold{abs}& 72\verb$\<bar> \<bar>$\\ 73\indexboldpos{\isasymle}{$HOL2arithrel}& 74\isadxboldpos{<=}{$HOL2arithrel}& 75\verb$\<le>$\\ 76\indexboldpos{\isasymtimes}{$Isatype}& 77\ttindexboldpos{*}{$HOL2arithfun} & 78\verb$\<times>$\\ 79\indexboldpos{\isasymin}{$HOL3Set0a}& 80\ttindexboldpos{:}{$HOL3Set0b} & 81\verb$\<in>$\\ 82\isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} & 83\verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} & 84\verb$\<notin>$\\ 85\indexboldpos{\isasymsubseteq}{$HOL3Set0e}& 86\verb$<=$ & \verb$\<subseteq>$\\ 87\indexboldpos{\isasymsubset}{$HOL3Set0f}& 88\verb$<$ & \verb$\<subset>$\\ 89\indexboldpos{\isasymunion}{$HOL3Set1}& 90\ttindexbold{Un} & 91\verb$\<union>$\\ 92\indexboldpos{\isasyminter}{$HOL3Set1}& 93\ttindexbold{Int} & 94\verb$\<inter>$\\ 95\isasymUnion\index{$HOL3Set2@\isasymUnion|bold}& 96\ttindexbold{UN}, \ttindexbold{Union} & 97\verb$\<Union>$\\ 98\isasymInter\index{$HOL3Set2@\isasymInter|bold}& 99\ttindexbold{INT}, \ttindexbold{Inter} & 100\verb$\<Inter>$\\ 101\isactrlsup{\isacharasterisk}\index{$HOL4star@\isactrlsup{\isacharasterisk}|bold}& 102\verb$^*$\index{$HOL4star@\verb$^$\texttt{*}|bold} & 103\verb$\<^sup>*$\\ 104\isasyminverse\index{$HOL4inv@\isasyminverse|bold}& 105\verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} & 106\verb$\<inverse>$\\ 107\hline 108\end{tabular} 109\end{center} 110\caption{Mathematical Symbols, Their \textsc{ascii}-Equivalents and Internal Names} 111\label{tab:ascii} 112\end{table}\indexbold{ASCII@\textsc{ascii} symbols} 113 114\input{appendix.tex} 115 116\begin{table}[htbp] 117\begin{center} 118\begin{tabular}{@{}|lllllllll|@{}} 119\hline 120\texttt{ALL} & 121\texttt{BIT} & 122\texttt{CHR} & 123\texttt{EX} & 124\texttt{GREATEST} & 125\texttt{INT} & 126\texttt{Int} & 127\texttt{LEAST} & 128\texttt{O} \\ 129\texttt{OFCLASS} & 130\texttt{PI} & 131\texttt{PROP} & 132\texttt{SIGMA} & 133\texttt{SOME} & 134\texttt{THE} & 135\texttt{TYPE} & 136\texttt{UN} & 137\texttt{Un} \\ 138\texttt{WRT} & 139\texttt{case} & 140\texttt{choose} & 141\texttt{div} & 142\texttt{dvd} & 143\texttt{else} & 144\texttt{funcset} & 145\texttt{if} & 146\texttt{in} \\ 147\texttt{let} & 148\texttt{mem} & 149\texttt{mod} & 150\texttt{o} & 151\texttt{of} & 152\texttt{op} & 153\texttt{then} &&\\ 154\hline 155\end{tabular} 156\end{center} 157\caption{Reserved Words in HOL Terms} 158\label{tab:ReservedWords} 159\end{table} 160 161 162%\begin{table}[htbp] 163%\begin{center} 164%\begin{tabular}{|lllll|} 165%\hline 166%\texttt{and} & 167%\texttt{binder} & 168%\texttt{concl} & 169%\texttt{congs} \\ 170%\texttt{distinct} & 171%\texttt{files} & 172%\texttt{in} & 173%\texttt{induction} & 174%\texttt{infixl} \\ 175%\texttt{infixr} & 176%\texttt{inject} & 177%\texttt{intrs} & 178%\texttt{is} & 179%\texttt{monos} \\ 180%\texttt{output} & 181%\texttt{where} & 182% & 183% & 184% \\ 185%\hline 186%\end{tabular} 187%\end{center} 188%\caption{Minor Keywords in HOL Theories} 189%\label{tab:keywords} 190%\end{table} 191