doc-src/TutorialI/appendix.tex
author wenzelm
Tue May 09 15:10:25 2000 +0200 (2000-05-09)
changeset 8845 03a2ae3059da
parent 8771 026f37a86ea7
child 9541 d17c0b34d5c8
permissions -rw-r--r--
updated keywords;
     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@\isasymuniqex|bold} &
    20 \isasymuniqex \\
    21 \texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
    22 \texttt{|}\index{$HOL0or@\ttor|bold} &
    23 \ttindexboldpos{-->}{$HOL0imp} &
    24 \verb$~$\index{$HOL0not@\verb$~$|bold} &
    25 \verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
    26 \ttindexbold{ALL} &
    27 \texttt{!}\index{$HOL0All@\ttall|bold} &
    28 \ttindexbold{EX} &
    29 \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
    30 \ttEXU\index{EXX@\ttEXU|bold} &
    31 \ttuniquex\index{$HOL0ExU@\ttuniquex|bold}\\
    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@\ttlbr|bold} &
    45 \texttt{|]}\index{$Isabrr@\ttrbr|bold} &
    46 \ttindexboldpos{==>}{$IsaImp} &
    47 \texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
    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 ASCII-equivalents}
    82 \label{fig:ascii}
    83 \end{figure}\indexbold{ASCII symbols}
    84 
    85 
    86 \begin{figure}[htbp]
    87 \begin{center}
    88 \begin{tabular}{|lllll|}
    89 \hline
    90 \texttt{ALL} &
    91 \texttt{case} &
    92 \texttt{div} &
    93 \texttt{dvd} &
    94 \texttt{else} \\
    95 \texttt{EX} &
    96 \texttt{if} &
    97 \texttt{in} &
    98 \texttt{INT} &
    99 \texttt{Int} \\
   100 \texttt{LEAST} &
   101 \texttt{let} &
   102 \texttt{mod} &
   103 \texttt{O} &
   104 \texttt{o} \\
   105 \texttt{of} &
   106 \texttt{op} &
   107 \texttt{PROP} &
   108 \texttt{SIGMA} &
   109 \texttt{then} \\
   110 \texttt{Times} &
   111 \texttt{UN} &
   112 \texttt{Un} &&\\
   113 \hline
   114 \end{tabular}
   115 \end{center}
   116 \caption{Reserved words in HOL terms}
   117 \label{fig:ReservedWords}
   118 \end{figure}
   119 
   120 
   121 \begin{figure}[htbp]
   122 
   123 %FIXME too long to be useful!??
   124 \begin{center}
   125 \begin{tabular}{|lll|}
   126 \hline
   127 \texttt{ML} &
   128 \texttt{ML_command} &
   129 \texttt{ML_setup} \\
   130 \texttt{also} &
   131 \texttt{apply} &
   132 \texttt{apply_end} \\
   133 \texttt{arities} &
   134 \texttt{assume} &
   135 \texttt{axclass} \\
   136 \texttt{axioms} &
   137 \texttt{back} &
   138 \texttt{by} \\
   139 \texttt{cannot_undo} &
   140 \texttt{case} &
   141 \texttt{cd} \\
   142 \texttt{chapter} &
   143 \texttt{classes} &
   144 \texttt{classrel} \\
   145 \texttt{clear_undos} &
   146 \texttt{coinductive} &
   147 \texttt{commit} \\
   148 \texttt{constdefs} &
   149 \texttt{consts} &
   150 \texttt{context} \\
   151 \texttt{datatype} &
   152 \texttt{def} &
   153 \texttt{defaultsort} \\
   154 \texttt{defer} &
   155 \texttt{defer_recdef} &
   156 \texttt{defs} \\
   157 \texttt{disable_pr} &
   158 \texttt{enable_pr} &
   159 \texttt{end} \\
   160 \texttt{exit} &
   161 \texttt{finally} &
   162 \texttt{fix} \\
   163 \texttt{from} &
   164 \texttt{global} &
   165 \texttt{have} \\
   166 \texttt{header} &
   167 \texttt{help} &
   168 \texttt{hence} \\
   169 \texttt{hide} &
   170 \texttt{inductive} &
   171 \texttt{inductive_cases} \\
   172 \texttt{init_toplevel} &
   173 \texttt{instance} &
   174 \texttt{judgment} \\
   175 \texttt{kill} &
   176 \texttt{kill_thy} &
   177 \texttt{lemma} \\
   178 \texttt{lemmas} &
   179 \texttt{let} &
   180 \texttt{local} \\
   181 \texttt{moreover} &
   182 \texttt{next} &
   183 \texttt{nonterminals} \\
   184 \texttt{note} &
   185 \texttt{obtain} &
   186 \texttt{oops} \\
   187 \texttt{oracle} &
   188 \texttt{parse_ast_translation} &
   189 \texttt{parse_translation} \\
   190 \texttt{pr} &
   191 \texttt{prefer} &
   192 \texttt{presume} \\
   193 \texttt{pretty_setmargin} &
   194 \texttt{primrec} &
   195 \texttt{print_ast_translation} \\
   196 \texttt{print_attributes} &
   197 \texttt{print_binds} &
   198 \texttt{print_cases} \\
   199 \texttt{print_claset} &
   200 \texttt{print_context} &
   201 \texttt{print_facts} \\
   202 \texttt{print_methods} &
   203 \texttt{print_simpset} &
   204 \texttt{print_syntax} \\
   205 \texttt{print_theorems} &
   206 \texttt{print_theory} &
   207 \texttt{print_translation} \\
   208 \texttt{proof} &
   209 \texttt{prop} &
   210 \texttt{pwd} \\
   211 \texttt{qed} &
   212 \texttt{quit} &
   213 \texttt{recdef} \\
   214 \texttt{record} &
   215 \texttt{redo} &
   216 \texttt{remove_thy} \\
   217 \texttt{rep_datatype} &
   218 \texttt{sect} &
   219 \texttt{section} \\
   220 \texttt{setup} &
   221 \texttt{show} &
   222 \texttt{sorry} \\
   223 \texttt{subsect} &
   224 \texttt{subsection} &
   225 \texttt{subsubsect} \\
   226 \texttt{subsubsection} &
   227 \texttt{syntax} &
   228 \texttt{term} \\
   229 \texttt{text} &
   230 \texttt{text_raw} &
   231 \texttt{then} \\
   232 \texttt{theorem} &
   233 \texttt{theorems} &
   234 \texttt{theory} \\
   235 \texttt{thm} &
   236 \texttt{thms_containing} &
   237 \texttt{thus} \\
   238 \texttt{token_translation} &
   239 \texttt{touch_all_thys} &
   240 \texttt{touch_child_thys} \\
   241 \texttt{touch_thy} &
   242 \texttt{translations} &
   243 \texttt{txt} \\
   244 \texttt{txt_raw} &
   245 \texttt{typ} &
   246 \texttt{typed_print_translation} \\
   247 \texttt{typedecl} &
   248 \texttt{typedef} &
   249 \texttt{types} \\
   250 \texttt{ultimately} &
   251 \texttt{undo} &
   252 \texttt{undos_proof} \\
   253 \texttt{update_thy} &
   254 \texttt{update_thy_only} &
   255 \texttt{use} \\
   256 \texttt{use_thy} &
   257 \texttt{use_thy_only} &
   258 \texttt{welcome} \\
   259 \texttt{with} &
   260  &
   261  \\
   262 \hline
   263 \end{tabular}
   264 \end{center}
   265 
   266 \begin{center}
   267 \begin{tabular}{|lllll|}
   268 \hline
   269 \texttt{and} &
   270 \texttt{binder} &
   271 \texttt{con_defs} &
   272 \texttt{concl} &
   273 \texttt{congs} \\
   274 \texttt{distinct} &
   275 \texttt{files} &
   276 \texttt{in} &
   277 \texttt{induction} &
   278 \texttt{infixl} \\
   279 \texttt{infixr} &
   280 \texttt{inject} &
   281 \texttt{intrs} &
   282 \texttt{is} &
   283 \texttt{monos} \\
   284 \texttt{output} &
   285 \texttt{where} &
   286  &
   287  &
   288  \\
   289 \hline
   290 \end{tabular}
   291 \end{center}
   292 
   293 
   294 \caption{Commands and minor keywords in HOL theories}
   295 \label{fig:keywords}
   296 \end{figure}