doc-src/Tutorial/appendix.tex
changeset 5375 1463e182c533
child 5581 295bb029170c
equal deleted inserted replaced
5374:6ef3742b6153 5375:1463e182c533
       
     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}