updated keywords;
authorwenzelm
Tue May 09 15:10:25 2000 +0200 (2000-05-09)
changeset 884503a2ae3059da
parent 8844 db71c334e854
child 8846 c7d945398677
updated keywords;
doc-src/TutorialI/appendix.tex
     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}