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}


83 
\end{figure}


84 


85 
\begin{figure}[htbp]


86 
\begin{center}


87 
\begin{tabular}{lllll}


88 
\hline


89 
\texttt{and} &


90 
\texttt{arities} &


91 
\texttt{assumes} &


92 
\texttt{axclass} &


93 
\texttt{binder} \\


94 
\texttt{classes} &


95 
\texttt{constdefs} &


96 
\texttt{consts} &


97 
\texttt{default} &


98 
\texttt{defines} \\


99 
\texttt{defs} &


100 
\texttt{end} &


101 
\texttt{fixes} &


102 
\texttt{global} &


103 
\texttt{inductive} \\


104 
\texttt{infixl} &


105 
\texttt{infixr} &


106 
\texttt{instance} &


107 
\texttt{local} &


108 
\texttt{locale} \\


109 
\texttt{mixfix} &


110 
\texttt{ML} &


111 
\texttt{MLtext} &


112 
\texttt{nonterminals} &


113 
\texttt{oracle} \\


114 
\texttt{output} &


115 
\texttt{path} &


116 
\texttt{primrec} &


117 
\texttt{rules} &


118 
\texttt{setup} \\


119 
\texttt{syntax} &


120 
\texttt{translations} &


121 
\texttt{typedef} &


122 
\texttt{types} &\\


123 
\hline


124 
\end{tabular}


125 
\end{center}


126 
\caption{Keywords in theory files}


127 
\label{fig:keywords}


128 
\end{figure}


129 


130 
\begin{figure}[htbp]


131 
\begin{center}


132 
\begin{tabular}{lllll}


133 
\hline


134 
\texttt{ALL} &


135 
\texttt{case} &


136 
\texttt{div} &


137 
\texttt{dvd} &


138 
\texttt{else} \\


139 
\texttt{EX} &


140 
\texttt{if} &


141 
\texttt{in} &


142 
\texttt{INT} &


143 
\texttt{Int} \\


144 
\texttt{LEAST} &


145 
\texttt{let} &


146 
\texttt{mod} &


147 
\texttt{O} &


148 
\texttt{o} \\


149 
\texttt{of} &


150 
\texttt{op} &


151 
\texttt{PROP} &


152 
\texttt{SIGMA} &


153 
\texttt{then} \\


154 
\texttt{Times} &


155 
\texttt{UN} &


156 
\texttt{Un} &&\\


157 
\hline


158 
\end{tabular}


159 
\end{center}


160 
\caption{Reserved words in HOL}


161 
\label{fig:ReservedWords}


162 
\end{figure}
