wneuper/isa: doc-src/TutorialI/appendix.tex@d17c0b34d5c8

     1 \appendix

     3 \chapter{Appendix}

     4 \label{sec:Appendix}

     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}

    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}

   121 %\begin{figure}[htbp]

   122 %\begin{center}

   123 %\begin{tabular}{|lllll|}

   124 %\hline

   125 %\texttt{and} &

   126 %\texttt{binder} &

   127 %\texttt{con_defs} &

   128 %\texttt{concl} &

   129 %\texttt{congs} \\

   130 %\texttt{distinct} &

   131 %\texttt{files} &

   132 %\texttt{in} &

   133 %\texttt{induction} &

   134 %\texttt{infixl} \\

   135 %\texttt{infixr} &

   136 %\texttt{inject} &

   137 %\texttt{intrs} &

   138 %\texttt{is} &

   139 %\texttt{monos} \\

   140 %\texttt{output} &

   141 %\texttt{where} &

   142 % &

   143 % &

   144 % \\

   145 %\hline

   146 %\end{tabular}

   147 %\end{center}

   148 %\caption{Minor keywords in HOL theories}

   149 %\label{fig:keywords}

   150 %\end{figure}

author	nipkow
	Sun, 06 Aug 2000 15:26:53 +0200
changeset 9541	d17c0b34d5c8
parent 8845	03a2ae3059da
child 9933	9feb1e0c4cb3
permissions	-rw-r--r--