doc-src/Tutorial/appendix.tex
author nipkow
Wed, 26 Aug 1998 16:57:49 +0200
changeset 5375 1463e182c533
child 5581 295bb029170c
permissions -rw-r--r--
The HOL tutorial.
     1 \appendix
     2 
     3 \chapter{Appendix}
     4 \label{sec:Appendix}
     5 
     6 \begin{figure}[htbp]
     7 \begin{center}
     8 \begin{tabular}{|llll|}
     9 \hline
    10 \texttt{arities} &
    11 \texttt{binder} &
    12 \texttt{classes} &
    13 \texttt{consts} \\
    14 \texttt{default} &
    15 \texttt{defs} &
    16 \texttt{end} &
    17 \texttt{global} \\
    18 \texttt{infixl} &
    19 \texttt{infixr} &
    20 \texttt{instance} &
    21 \texttt{local} \\
    22 \texttt{mixfix} &
    23 \texttt{ML} &
    24 \texttt{MLtext} &
    25 \texttt{nonterminals} \\
    26 \texttt{oracle} &
    27 \texttt{output} &
    28 \texttt{path} &
    29 \texttt{rules} \\
    30 \texttt{setup} &
    31 \texttt{syntax} &
    32 \texttt{translations} &
    33 \texttt{types} \\
    34 \texttt{constdefs} &
    35 \texttt{axclass} &&\\
    36 \hline
    37 \end{tabular}
    38 \end{center}
    39 \caption{Keywords in theory files}
    40 \label{fig:keywords}
    41 \end{figure}
    42 
    43 \begin{figure}[htbp]
    44 \begin{center}
    45 \begin{tabular}{|lllll|}
    46 \hline
    47 \texttt{ALL} &
    48 \texttt{case} &
    49 \texttt{div} &
    50 \texttt{dvd} &
    51 \texttt{else} \\
    52 \texttt{EX} &
    53 \texttt{if} &
    54 \texttt{in} &
    55 \texttt{INT} &
    56 \texttt{Int} \\
    57 \texttt{LEAST} &
    58 \texttt{let} &
    59 \texttt{mod} &
    60 \texttt{O} &
    61 \texttt{o} \\
    62 \texttt{of} &
    63 \texttt{op} &
    64 \texttt{PROP} &
    65 \texttt{SIGMA} &
    66 \texttt{then} \\
    67 \texttt{Times} &
    68 \texttt{UN} &
    69 \texttt{Un} &&\\
    70 \hline
    71 \end{tabular}
    72 \end{center}
    73 \caption{Reserved words in HOL}
    74 \label{fig:ReservedWords}
    75 \end{figure}