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}