8743

1 
\appendix


2 


3 
\chapter{Appendix}


4 
\label{sec:Appendix}


5 


6 
\begin{figure}[htbp]


7 
\begin{center}


8 
\begin{tabular}{ccccccccccc}


9 
\hline


10 
\indexboldpos{\isasymand}{$HOL0and} &


11 
\indexboldpos{\isasymor}{$HOL0or} &


12 
\indexboldpos{\isasymimp}{$HOL0imp} &


13 
\indexboldpos{\isasymnot}{$HOL0not} &


14 
\indexboldpos{\isasymnoteq}{$HOL0noteq} &


15 
\indexboldpos{\isasymforall}{$HOL0All} &


16 
\isasymforall &


17 
\indexboldpos{\isasymexists}{$HOL0Ex} &


18 
\isasymexists &


19 
\isasymuniqex\index{$HOL0ExU@\isasymuniqexbold} &


20 
\isasymuniqex \\


21 
\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &


22 
\texttt{}\index{$HOL0or@\ttorbold} &


23 
\ttindexboldpos{>}{$HOL0imp} &


24 
\verb$~$\index{$HOL0not@\verb$~$bold} &


25 
\verb$~=$\index{$HOL0noteq@\verb$~=$bold} &


26 
\ttindexbold{ALL} &


27 
\texttt{!}\index{$HOL0All@\ttallbold} &


28 
\ttindexbold{EX} &


29 
\texttt{?}\index{$HOL0Ex@\texttt{?}bold} &


30 
\ttEXU\index{EXX@\ttEXUbold} &


31 
\ttuniquex\index{$HOL0ExU@\ttuniquexbold}\\


32 
\hline\hline


33 
\indexboldpos{\isasymlbrakk}{$Isabrl} &


34 
\indexboldpos{\isasymrbrakk}{$Isabrr} &


35 
\indexboldpos{\isasymImp}{$IsaImp} &


36 
\indexboldpos{\isasymAnd}{$IsaAnd} &


37 
\indexboldpos{\isasymequiv}{$IsaEq} &


38 
\indexboldpos{\isasymlambda}{$Isalam} &


39 
\indexboldpos{\isasymFun}{$IsaFun}&


40 
&


41 
&


42 
&


43 
\\


44 
\texttt{[}\index{$Isabrl@\ttlbrbold} &


45 
\texttt{]}\index{$Isabrr@\ttrbrbold} &


46 
\ttindexboldpos{==>}{$IsaImp} &


47 
\texttt{!!}\index{$IsaAnd@\ttAndbold} &


48 
\ttindexboldpos{==}{$IsaEq} &


49 
\texttt{\%}\indexbold{$Isalam@\texttt{\%}} &


50 
\ttindexboldpos{=>}{$IsaFun}&


51 
&


52 
&


53 
&


54 
\\


55 
\hline\hline


56 
\indexboldpos{\isasymcirc}{$HOL1} &


57 
\indexboldpos{\isasymle}{$HOL2arithrel}&


58 
&


59 
&


60 
&


61 
&


62 
&


63 
&


64 
&


65 
&


66 
\\


67 
\ttindexbold{o} &


68 
\ttindexboldpos{<=}{$HOL2arithrel}&


69 
&


70 
&


71 
&


72 
&


73 
&


74 
&


75 
&


76 
&


77 
\\


78 
\hline


79 
\end{tabular}


80 
\end{center}


81 
\caption{Mathematical symbols and their ASCIIequivalents}


82 
\label{fig:ascii}

8771

83 
\end{figure}\indexbold{ASCII symbols}

8743

84 


85 


86 
\begin{figure}[htbp]


87 
\begin{center}


88 
\begin{tabular}{lllll}


89 
\hline


90 
\texttt{ALL} &


91 
\texttt{case} &


92 
\texttt{div} &


93 
\texttt{dvd} &


94 
\texttt{else} \\


95 
\texttt{EX} &


96 
\texttt{if} &


97 
\texttt{in} &


98 
\texttt{INT} &


99 
\texttt{Int} \\


100 
\texttt{LEAST} &


101 
\texttt{let} &


102 
\texttt{mod} &


103 
\texttt{O} &


104 
\texttt{o} \\


105 
\texttt{of} &


106 
\texttt{op} &


107 
\texttt{PROP} &


108 
\texttt{SIGMA} &


109 
\texttt{then} \\


110 
\texttt{Times} &


111 
\texttt{UN} &


112 
\texttt{Un} &&\\


113 
\hline


114 
\end{tabular}


115 
\end{center}

8845

116 
\caption{Reserved words in HOL terms}

8743

117 
\label{fig:ReservedWords}


118 
\end{figure}

8845

119 


120 

9541

121 
%\begin{figure}[htbp]


122 
%\begin{center}


123 
%\begin{tabular}{lllll}


124 
%\hline


125 
%\texttt{and} &


126 
%\texttt{binder} &


127 
%\texttt{con_defs} &


128 
%\texttt{concl} &


129 
%\texttt{congs} \\


130 
%\texttt{distinct} &


131 
%\texttt{files} &


132 
%\texttt{in} &


133 
%\texttt{induction} &


134 
%\texttt{infixl} \\


135 
%\texttt{infixr} &


136 
%\texttt{inject} &


137 
%\texttt{intrs} &


138 
%\texttt{is} &


139 
%\texttt{monos} \\


140 
%\texttt{output} &


141 
%\texttt{where} &


142 
% &


143 
% &


144 
% \\


145 
%\hline


146 
%\end{tabular}


147 
%\end{center}


148 
%\caption{Minor keywords in HOL theories}


149 
%\label{fig:keywords}


150 
%\end{figure}
