1.1 --- a/doc-src/TutorialI/appendix.tex Tue May 09 14:33:43 2000 +0200
1.2 +++ b/doc-src/TutorialI/appendix.tex Tue May 09 15:10:25 2000 +0200
1.3 @@ -82,50 +82,6 @@
1.4 \label{fig:ascii}
1.5 \end{figure}\indexbold{ASCII symbols}
1.6
1.7 -\begin{figure}[htbp]
1.8 -\begin{center}
1.9 -\begin{tabular}{|lllll|}
1.10 -\hline
1.11 -\texttt{and} &
1.12 -\texttt{arities} &
1.13 -\texttt{assumes} &
1.14 -\texttt{axclass} &
1.15 -\texttt{binder} \\
1.16 -\texttt{classes} &
1.17 -\texttt{constdefs} &
1.18 -\texttt{consts} &
1.19 -\texttt{default} &
1.20 -\texttt{defines} \\
1.21 -\texttt{defs} &
1.22 -\texttt{end} &
1.23 -\texttt{fixes} &
1.24 -\texttt{global} &
1.25 -\texttt{inductive} \\
1.26 -\texttt{infixl} &
1.27 -\texttt{infixr} &
1.28 -\texttt{instance} &
1.29 -\texttt{local} &
1.30 -\texttt{locale} \\
1.31 -\texttt{mixfix} &
1.32 -\texttt{ML} &
1.33 -\texttt{MLtext} &
1.34 -\texttt{nonterminals} &
1.35 -\texttt{oracle} \\
1.36 -\texttt{output} &
1.37 -\texttt{path} &
1.38 -\texttt{primrec} &
1.39 -\texttt{rules} &
1.40 -\texttt{setup} \\
1.41 -\texttt{syntax} &
1.42 -\texttt{translations} &
1.43 -\texttt{typedef} &
1.44 -\texttt{types} &\\
1.45 -\hline
1.46 -\end{tabular}
1.47 -\end{center}
1.48 -\caption{Keywords in theory files}
1.49 -\label{fig:keywords}
1.50 -\end{figure}
1.51
1.52 \begin{figure}[htbp]
1.53 \begin{center}
1.54 @@ -157,6 +113,184 @@
1.55 \hline
1.56 \end{tabular}
1.57 \end{center}
1.58 -\caption{Reserved words in HOL}
1.59 +\caption{Reserved words in HOL terms}
1.60 \label{fig:ReservedWords}
1.61 \end{figure}
1.62 +
1.63 +
1.64 +\begin{figure}[htbp]
1.65 +
1.66 +%FIXME too long to be useful!??
1.67 +\begin{center}
1.68 +\begin{tabular}{|lll|}
1.69 +\hline
1.70 +\texttt{ML} &
1.71 +\texttt{ML_command} &
1.72 +\texttt{ML_setup} \\
1.73 +\texttt{also} &
1.74 +\texttt{apply} &
1.75 +\texttt{apply_end} \\
1.76 +\texttt{arities} &
1.77 +\texttt{assume} &
1.78 +\texttt{axclass} \\
1.79 +\texttt{axioms} &
1.80 +\texttt{back} &
1.81 +\texttt{by} \\
1.82 +\texttt{cannot_undo} &
1.83 +\texttt{case} &
1.84 +\texttt{cd} \\
1.85 +\texttt{chapter} &
1.86 +\texttt{classes} &
1.87 +\texttt{classrel} \\
1.88 +\texttt{clear_undos} &
1.89 +\texttt{coinductive} &
1.90 +\texttt{commit} \\
1.91 +\texttt{constdefs} &
1.92 +\texttt{consts} &
1.93 +\texttt{context} \\
1.94 +\texttt{datatype} &
1.95 +\texttt{def} &
1.96 +\texttt{defaultsort} \\
1.97 +\texttt{defer} &
1.98 +\texttt{defer_recdef} &
1.99 +\texttt{defs} \\
1.100 +\texttt{disable_pr} &
1.101 +\texttt{enable_pr} &
1.102 +\texttt{end} \\
1.103 +\texttt{exit} &
1.104 +\texttt{finally} &
1.105 +\texttt{fix} \\
1.106 +\texttt{from} &
1.107 +\texttt{global} &
1.108 +\texttt{have} \\
1.109 +\texttt{header} &
1.110 +\texttt{help} &
1.111 +\texttt{hence} \\
1.112 +\texttt{hide} &
1.113 +\texttt{inductive} &
1.114 +\texttt{inductive_cases} \\
1.115 +\texttt{init_toplevel} &
1.116 +\texttt{instance} &
1.117 +\texttt{judgment} \\
1.118 +\texttt{kill} &
1.119 +\texttt{kill_thy} &
1.120 +\texttt{lemma} \\
1.121 +\texttt{lemmas} &
1.122 +\texttt{let} &
1.123 +\texttt{local} \\
1.124 +\texttt{moreover} &
1.125 +\texttt{next} &
1.126 +\texttt{nonterminals} \\
1.127 +\texttt{note} &
1.128 +\texttt{obtain} &
1.129 +\texttt{oops} \\
1.130 +\texttt{oracle} &
1.131 +\texttt{parse_ast_translation} &
1.132 +\texttt{parse_translation} \\
1.133 +\texttt{pr} &
1.134 +\texttt{prefer} &
1.135 +\texttt{presume} \\
1.136 +\texttt{pretty_setmargin} &
1.137 +\texttt{primrec} &
1.138 +\texttt{print_ast_translation} \\
1.139 +\texttt{print_attributes} &
1.140 +\texttt{print_binds} &
1.141 +\texttt{print_cases} \\
1.142 +\texttt{print_claset} &
1.143 +\texttt{print_context} &
1.144 +\texttt{print_facts} \\
1.145 +\texttt{print_methods} &
1.146 +\texttt{print_simpset} &
1.147 +\texttt{print_syntax} \\
1.148 +\texttt{print_theorems} &
1.149 +\texttt{print_theory} &
1.150 +\texttt{print_translation} \\
1.151 +\texttt{proof} &
1.152 +\texttt{prop} &
1.153 +\texttt{pwd} \\
1.154 +\texttt{qed} &
1.155 +\texttt{quit} &
1.156 +\texttt{recdef} \\
1.157 +\texttt{record} &
1.158 +\texttt{redo} &
1.159 +\texttt{remove_thy} \\
1.160 +\texttt{rep_datatype} &
1.161 +\texttt{sect} &
1.162 +\texttt{section} \\
1.163 +\texttt{setup} &
1.164 +\texttt{show} &
1.165 +\texttt{sorry} \\
1.166 +\texttt{subsect} &
1.167 +\texttt{subsection} &
1.168 +\texttt{subsubsect} \\
1.169 +\texttt{subsubsection} &
1.170 +\texttt{syntax} &
1.171 +\texttt{term} \\
1.172 +\texttt{text} &
1.173 +\texttt{text_raw} &
1.174 +\texttt{then} \\
1.175 +\texttt{theorem} &
1.176 +\texttt{theorems} &
1.177 +\texttt{theory} \\
1.178 +\texttt{thm} &
1.179 +\texttt{thms_containing} &
1.180 +\texttt{thus} \\
1.181 +\texttt{token_translation} &
1.182 +\texttt{touch_all_thys} &
1.183 +\texttt{touch_child_thys} \\
1.184 +\texttt{touch_thy} &
1.185 +\texttt{translations} &
1.186 +\texttt{txt} \\
1.187 +\texttt{txt_raw} &
1.188 +\texttt{typ} &
1.189 +\texttt{typed_print_translation} \\
1.190 +\texttt{typedecl} &
1.191 +\texttt{typedef} &
1.192 +\texttt{types} \\
1.193 +\texttt{ultimately} &
1.194 +\texttt{undo} &
1.195 +\texttt{undos_proof} \\
1.196 +\texttt{update_thy} &
1.197 +\texttt{update_thy_only} &
1.198 +\texttt{use} \\
1.199 +\texttt{use_thy} &
1.200 +\texttt{use_thy_only} &
1.201 +\texttt{welcome} \\
1.202 +\texttt{with} &
1.203 + &
1.204 + \\
1.205 +\hline
1.206 +\end{tabular}
1.207 +\end{center}
1.208 +
1.209 +\begin{center}
1.210 +\begin{tabular}{|lllll|}
1.211 +\hline
1.212 +\texttt{and} &
1.213 +\texttt{binder} &
1.214 +\texttt{con_defs} &
1.215 +\texttt{concl} &
1.216 +\texttt{congs} \\
1.217 +\texttt{distinct} &
1.218 +\texttt{files} &
1.219 +\texttt{in} &
1.220 +\texttt{induction} &
1.221 +\texttt{infixl} \\
1.222 +\texttt{infixr} &
1.223 +\texttt{inject} &
1.224 +\texttt{intrs} &
1.225 +\texttt{is} &
1.226 +\texttt{monos} \\
1.227 +\texttt{output} &
1.228 +\texttt{where} &
1.229 + &
1.230 + &
1.231 + \\
1.232 +\hline
1.233 +\end{tabular}
1.234 +\end{center}
1.235 +
1.236 +
1.237 +\caption{Commands and minor keywords in HOL theories}
1.238 +\label{fig:keywords}
1.239 +\end{figure}