doc-src/TutorialI/appendix.tex
author nipkow
Wed Apr 19 11:54:39 2000 +0200 (2000-04-19)
changeset 8743 3253c6046d57
child 8771 026f37a86ea7
permissions -rw-r--r--
I wonder if that's all?
     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}
    84 
    85 \begin{figure}[htbp]
    86 \begin{center}
    87 \begin{tabular}{|lllll|}
    88 \hline
    89 \texttt{and} &
    90 \texttt{arities} &
    91 \texttt{assumes} &
    92 \texttt{axclass} &
    93 \texttt{binder} \\
    94 \texttt{classes} &
    95 \texttt{constdefs} &
    96 \texttt{consts} &
    97 \texttt{default} &
    98 \texttt{defines} \\
    99 \texttt{defs} &
   100 \texttt{end} &
   101 \texttt{fixes} &
   102 \texttt{global} &
   103 \texttt{inductive} \\
   104 \texttt{infixl} &
   105 \texttt{infixr} &
   106 \texttt{instance} &
   107 \texttt{local} &
   108 \texttt{locale} \\
   109 \texttt{mixfix} &
   110 \texttt{ML} &
   111 \texttt{MLtext} &
   112 \texttt{nonterminals} &
   113 \texttt{oracle} \\
   114 \texttt{output} &
   115 \texttt{path} &
   116 \texttt{primrec} &
   117 \texttt{rules} &
   118 \texttt{setup} \\
   119 \texttt{syntax} &
   120 \texttt{translations} &
   121 \texttt{typedef} &
   122 \texttt{types} &\\
   123 \hline
   124 \end{tabular}
   125 \end{center}
   126 \caption{Keywords in theory files}
   127 \label{fig:keywords}
   128 \end{figure}
   129 
   130 \begin{figure}[htbp]
   131 \begin{center}
   132 \begin{tabular}{|lllll|}
   133 \hline
   134 \texttt{ALL} &
   135 \texttt{case} &
   136 \texttt{div} &
   137 \texttt{dvd} &
   138 \texttt{else} \\
   139 \texttt{EX} &
   140 \texttt{if} &
   141 \texttt{in} &
   142 \texttt{INT} &
   143 \texttt{Int} \\
   144 \texttt{LEAST} &
   145 \texttt{let} &
   146 \texttt{mod} &
   147 \texttt{O} &
   148 \texttt{o} \\
   149 \texttt{of} &
   150 \texttt{op} &
   151 \texttt{PROP} &
   152 \texttt{SIGMA} &
   153 \texttt{then} \\
   154 \texttt{Times} &
   155 \texttt{UN} &
   156 \texttt{Un} &&\\
   157 \hline
   158 \end{tabular}
   159 \end{center}
   160 \caption{Reserved words in HOL}
   161 \label{fig:ReservedWords}
   162 \end{figure}