\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{\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} &

\verb$\<epsilon>$\\

\indexboldpos{\isasymcirc}{$HOL1} &

\ttindexbold{o} &

\verb$\<circ>$\\

\indexboldpos{\isasymbar~\isasymbar}{$HOL2arithfun}&

\ttindexbold{abs}&

\verb$\<bar> \<bar>$\\

\indexboldpos{\isasymle}{$HOL2arithrel}&

\ttindexboldpos{<=}{$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 ASCII-equivalents and X-Symbol codes}

\label{tab:ascii}

\end{table}\indexbold{ASCII symbols}

\input{Misc/document/appendix.tex}

\begin{table}[htbp]

\begin{center}

\begin{tabular}{|lllllllll|}

\hline

\texttt{ALL} &

\texttt{BIT} &

\texttt{CHR} &

\texttt{EX} &

\texttt{GOAL} &

\texttt{INT} &

\texttt{Int} &

\texttt{LEAST} &

\texttt{O} \\

\texttt{OFCLASS} &

\texttt{PI} &

\texttt{PROP} &

\texttt{SIGMA} &

\texttt{SOME} &

\texttt{TYPE} &

\texttt{UN} &

\texttt{Un} &\\

\texttt{case} &

\texttt{choose} &

\texttt{div} &

\texttt{dvd} &

\texttt{else} &

\texttt{funcset} &

\texttt{if} &

\texttt{in} &

\texttt{lam} \\

\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{con_defs} &

%\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}