doc-src/TutorialI/appendix.tex
 changeset 8743 3253c6046d57 child 8771 026f37a86ea7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/TutorialI/appendix.tex	Wed Apr 19 11:54:39 2000 +0200
1.3 @@ -0,0 +1,162 @@
1.4 +\appendix
1.5 +
1.6 +\chapter{Appendix}
1.7 +\label{sec:Appendix}
1.8 +
1.9 +\begin{figure}[htbp]
1.10 +\begin{center}
1.11 +\begin{tabular}{|ccccccccccc|}
1.12 +\hline
1.13 +\indexboldpos{\isasymand}{$HOL0and} & 1.14 +\indexboldpos{\isasymor}{$HOL0or} &
1.15 +\indexboldpos{\isasymimp}{$HOL0imp} & 1.16 +\indexboldpos{\isasymnot}{$HOL0not} &
1.17 +\indexboldpos{\isasymnoteq}{$HOL0noteq} & 1.18 +\indexboldpos{\isasymforall}{$HOL0All} &
1.19 +\isasymforall &
1.20 +\indexboldpos{\isasymexists}{$HOL0Ex} & 1.21 +\isasymexists & 1.22 +\isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
1.23 +\isasymuniqex \\
1.24 +\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} & 1.25 +\texttt{|}\index{$HOL0or@\ttor|bold} &
1.26 +\ttindexboldpos{-->}{$HOL0imp} & 1.27 +\verb$~$\index{$HOL0not@\verb$~$|bold} &
1.28 +\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} & 1.29 +\ttindexbold{ALL} & 1.30 +\texttt{!}\index{$HOL0All@\ttall|bold} &
1.31 +\ttindexbold{EX} &
1.32 +\texttt{?}\index{$HOL0Ex@\texttt{?}|bold} & 1.33 +\ttEXU\index{EXX@\ttEXU|bold} & 1.34 +\ttuniquex\index{$HOL0ExU@\ttuniquex|bold}\\
1.35 +\hline\hline
1.36 +\indexboldpos{\isasymlbrakk}{$Isabrl} & 1.37 +\indexboldpos{\isasymrbrakk}{$Isabrr} &
1.38 +\indexboldpos{\isasymImp}{$IsaImp} & 1.39 +\indexboldpos{\isasymAnd}{$IsaAnd} &
1.40 +\indexboldpos{\isasymequiv}{$IsaEq} & 1.41 +\indexboldpos{\isasymlambda}{$Isalam} &
1.42 +\indexboldpos{\isasymFun}{$IsaFun}& 1.43 +& 1.44 +& 1.45 +& 1.46 +\\ 1.47 +\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
1.48 +\texttt{|]}\index{$Isabrr@\ttrbr|bold} & 1.49 +\ttindexboldpos{==>}{$IsaImp} &
1.50 +\texttt{!!}\index{$IsaAnd@\ttAnd|bold} & 1.51 +\ttindexboldpos{==}{$IsaEq} &
1.52 +\texttt{\%}\indexbold{$Isalam@\texttt{\%}} & 1.53 +\ttindexboldpos{=>}{$IsaFun}&
1.54 +&
1.55 +&
1.56 +&
1.57 + \\
1.58 +\hline\hline
1.59 +\indexboldpos{\isasymcirc}{$HOL1} & 1.60 +\indexboldpos{\isasymle}{$HOL2arithrel}&
1.61 +&
1.62 +&
1.63 +&
1.64 +&
1.65 +&
1.66 +&
1.67 +&
1.68 +&
1.69 + \\
1.70 +\ttindexbold{o} &
1.71 +\ttindexboldpos{<=}{\$HOL2arithrel}&
1.72 +&
1.73 +&
1.74 +&
1.75 +&
1.76 +&
1.77 +&
1.78 +&
1.79 +&
1.80 +\\
1.81 +\hline
1.82 +\end{tabular}
1.83 +\end{center}
1.84 +\caption{Mathematical symbols and their ASCII-equivalents}
1.85 +\label{fig:ascii}
1.86 +\end{figure}
1.87 +
1.88 +\begin{figure}[htbp]
1.89 +\begin{center}
1.90 +\begin{tabular}{|lllll|}
1.91 +\hline
1.92 +\texttt{and} &
1.93 +\texttt{arities} &
1.94 +\texttt{assumes} &
1.95 +\texttt{axclass} &
1.96 +\texttt{binder} \\
1.97 +\texttt{classes} &
1.98 +\texttt{constdefs} &
1.99 +\texttt{consts} &
1.100 +\texttt{default} &
1.101 +\texttt{defines} \\
1.102 +\texttt{defs} &
1.103 +\texttt{end} &
1.104 +\texttt{fixes} &
1.105 +\texttt{global} &
1.106 +\texttt{inductive} \\
1.107 +\texttt{infixl} &
1.108 +\texttt{infixr} &
1.109 +\texttt{instance} &
1.110 +\texttt{local} &
1.111 +\texttt{locale} \\
1.112 +\texttt{mixfix} &
1.113 +\texttt{ML} &
1.114 +\texttt{MLtext} &
1.115 +\texttt{nonterminals} &
1.116 +\texttt{oracle} \\
1.117 +\texttt{output} &
1.118 +\texttt{path} &
1.119 +\texttt{primrec} &
1.120 +\texttt{rules} &
1.121 +\texttt{setup} \\
1.122 +\texttt{syntax} &
1.123 +\texttt{translations} &
1.124 +\texttt{typedef} &
1.125 +\texttt{types} &\\
1.126 +\hline
1.127 +\end{tabular}
1.128 +\end{center}
1.129 +\caption{Keywords in theory files}
1.130 +\label{fig:keywords}
1.131 +\end{figure}
1.132 +
1.133 +\begin{figure}[htbp]
1.134 +\begin{center}
1.135 +\begin{tabular}{|lllll|}
1.136 +\hline
1.137 +\texttt{ALL} &
1.138 +\texttt{case} &
1.139 +\texttt{div} &
1.140 +\texttt{dvd} &
1.141 +\texttt{else} \\
1.142 +\texttt{EX} &
1.143 +\texttt{if} &
1.144 +\texttt{in} &
1.145 +\texttt{INT} &
1.146 +\texttt{Int} \\
1.147 +\texttt{LEAST} &
1.148 +\texttt{let} &
1.149 +\texttt{mod} &
1.150 +\texttt{O} &
1.151 +\texttt{o} \\
1.152 +\texttt{of} &
1.153 +\texttt{op} &
1.154 +\texttt{PROP} &
1.155 +\texttt{SIGMA} &
1.156 +\texttt{then} \\
1.157 +\texttt{Times} &
1.158 +\texttt{UN} &
1.159 +\texttt{Un} &&\\
1.160 +\hline
1.161 +\end{tabular}
1.162 +\end{center}
1.163 +\caption{Reserved words in HOL}
1.164 +\label{fig:ReservedWords}
1.165 +\end{figure}