doc-src/TutorialI/appendix.tex
author huffman
Thu Apr 19 10:49:47 2012 +0200 (2012-04-19)
changeset 47579 28f6f4ad69bf
parent 15364 0c3891c3528f
child 48522 708278fc2dff
permissions -rw-r--r--
tuned lemmas (v)image_id;
removed duplicate of vimage_id
     1 \appendix
     2 
     3 \chapter{Appendix}
     4 \label{sec:Appendix}
     5 
     6 \begin{table}[htbp]
     7 \begin{center}
     8 \begin{tabular}{|l|l|l|}
     9 \hline
    10 \indexboldpos{\isasymlbrakk}{$Isabrl} &
    11 \texttt{[|}\index{$Isabrl@\ttlbr|bold} &
    12 \verb$\<lbrakk>$ \\
    13 \indexboldpos{\isasymrbrakk}{$Isabrr} &
    14 \texttt{|]}\index{$Isabrr@\ttrbr|bold} &
    15 \verb$\<rbrakk>$ \\
    16 \indexboldpos{\isasymImp}{$IsaImp} &
    17 \ttindexboldpos{==>}{$IsaImp} &
    18 \verb$\<Longrightarrow>$ \\
    19 \isasymAnd\index{$IsaAnd@\isasymAnd|bold}&
    20 \texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
    21 \verb$\<And>$ \\
    22 \indexboldpos{\isasymequiv}{$IsaEq} &
    23 \ttindexboldpos{==}{$IsaEq} &
    24 \verb$\<equiv>$ \\
    25 \indexboldpos{\isasymrightleftharpoons}{$IsaEqTrans} &
    26 \ttindexboldpos{==}{$IsaEq} &
    27 \verb$\<rightleftharpoons>$ \\
    28 \indexboldpos{\isasymrightharpoonup}{$IsaEqTrans1} &
    29 \ttindexboldpos{=>}{$IsaFun} &
    30 \verb$\<rightharpoonup>$ \\
    31 \indexboldpos{\isasymleftharpoondown}{$IsaEqTrans2} &
    32 \ttindexboldpos{<=}{$IsaFun2} &
    33 \verb$\<leftharpoondown>$ \\
    34 \indexboldpos{\isasymlambda}{$Isalam} &
    35 \texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
    36 \verb$\<lambda>$ \\
    37 \indexboldpos{\isasymFun}{$IsaFun} &
    38 \ttindexboldpos{=>}{$IsaFun} &
    39 \verb$\<Rightarrow>$ \\
    40 \indexboldpos{\isasymand}{$HOL0and} &
    41 \texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
    42 \verb$\<and>$ \\
    43 \indexboldpos{\isasymor}{$HOL0or} &
    44 \texttt{|}\index{$HOL0or@\ttor|bold} &
    45 \verb$\<or>$ \\
    46 \indexboldpos{\isasymimp}{$HOL0imp} &
    47 \ttindexboldpos{-->}{$HOL0imp} &
    48 \verb$\<longrightarrow>$ \\
    49 \indexboldpos{\isasymnot}{$HOL0not} &
    50 \verb$~$\index{$HOL0not@\verb$~$|bold} &
    51 \verb$\<not>$ \\
    52 \indexboldpos{\isasymnoteq}{$HOL0noteq} &
    53 \verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
    54 \verb$\<noteq>$ \\
    55 \indexboldpos{\isasymforall}{$HOL0All} &
    56 \ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} &
    57 \verb$\<forall>$ \\
    58 \indexboldpos{\isasymexists}{$HOL0Ex} &
    59 \ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
    60 \verb$\<exists>$ \\
    61 \isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
    62 \ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
    63 \verb$\<exists>!$\\
    64 \indexboldpos{\isasymepsilon}{$HOL0ExSome} &
    65 \ttindexbold{SOME}, \isa{\at}\index{$HOL2list@\isa{\at}} &
    66 \verb$\<epsilon>$\\
    67 \indexboldpos{\isasymcirc}{$HOL1} &
    68 \ttindexbold{o} &
    69 \verb$\<circ>$\\
    70 \indexboldpos{\isasymbar~\isasymbar}{$HOL2arithfun}&
    71 \ttindexbold{abs}&
    72 \verb$\<bar> \<bar>$\\
    73 \indexboldpos{\isasymle}{$HOL2arithrel}&
    74 \isadxboldpos{<=}{$HOL2arithrel}&
    75 \verb$\<le>$\\
    76 \indexboldpos{\isasymtimes}{$Isatype}&
    77 \ttindexboldpos{*}{$HOL2arithfun} &
    78 \verb$\<times>$\\
    79 \indexboldpos{\isasymin}{$HOL3Set0a}&
    80 \ttindexboldpos{:}{$HOL3Set0b} &
    81 \verb$\<in>$\\
    82 \isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} &
    83 \verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} &
    84 \verb$\<notin>$\\
    85 \indexboldpos{\isasymsubseteq}{$HOL3Set0e}&
    86 \verb$<=$ & \verb$\<subseteq>$\\
    87 \indexboldpos{\isasymsubset}{$HOL3Set0f}&
    88 \verb$<$ & \verb$\<subset>$\\
    89 \indexboldpos{\isasymunion}{$HOL3Set1}&
    90 \ttindexbold{Un} &
    91 \verb$\<union>$\\
    92 \indexboldpos{\isasyminter}{$HOL3Set1}&
    93 \ttindexbold{Int} &
    94 \verb$\<inter>$\\
    95 \isasymUnion\index{$HOL3Set2@\isasymUnion|bold}&
    96 \ttindexbold{UN}, \ttindexbold{Union} &
    97 \verb$\<Union>$\\
    98 \isasymInter\index{$HOL3Set2@\isasymInter|bold}&
    99 \ttindexbold{INT}, \ttindexbold{Inter} &
   100 \verb$\<Inter>$\\
   101 \isactrlsup{\isacharasterisk}\index{$HOL4star@\isactrlsup{\isacharasterisk}|bold}&
   102 \verb$^*$\index{$HOL4star@\verb$^$\texttt{*}|bold} &
   103 \verb$\<^sup>*$\\
   104 \isasyminverse\index{$HOL4inv@\isasyminverse|bold}&
   105 \verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} &
   106 \verb$\<inverse>$\\
   107 \hline
   108 \end{tabular}
   109 \end{center}
   110 \caption{Mathematical Symbols, Their \textsc{ascii}-Equivalents and Internal Names}
   111 \label{tab:ascii}
   112 \end{table}\indexbold{ASCII@\textsc{ascii} symbols}
   113 
   114 \input{Misc/document/appendix.tex}
   115 
   116 \begin{table}[htbp]
   117 \begin{center}
   118 \begin{tabular}{@{}|lllllllll|@{}}
   119 \hline
   120 \texttt{ALL} &
   121 \texttt{BIT} &
   122 \texttt{CHR} &
   123 \texttt{EX} &
   124 \texttt{GREATEST} &
   125 \texttt{INT} &
   126 \texttt{Int} &
   127 \texttt{LEAST} &
   128 \texttt{O} \\
   129 \texttt{OFCLASS} &
   130 \texttt{PI} &
   131 \texttt{PROP} &
   132 \texttt{SIGMA} &
   133 \texttt{SOME} &
   134 \texttt{THE} &
   135 \texttt{TYPE} &
   136 \texttt{UN} &
   137 \texttt{Un} \\
   138 \texttt{WRT} &
   139 \texttt{case} &
   140 \texttt{choose} &
   141 \texttt{div} &
   142 \texttt{dvd} &
   143 \texttt{else} &
   144 \texttt{funcset} &
   145 \texttt{if} &
   146 \texttt{in} \\
   147 \texttt{let} &
   148 \texttt{mem} &
   149 \texttt{mod} &
   150 \texttt{o} &
   151 \texttt{of} &
   152 \texttt{op} &
   153 \texttt{then} &&\\
   154 \hline
   155 \end{tabular}
   156 \end{center}
   157 \caption{Reserved Words in HOL Terms}
   158 \label{tab:ReservedWords}
   159 \end{table}
   160 
   161 
   162 %\begin{table}[htbp]
   163 %\begin{center}
   164 %\begin{tabular}{|lllll|}
   165 %\hline
   166 %\texttt{and} &
   167 %\texttt{binder} &
   168 %\texttt{concl} &
   169 %\texttt{congs} \\
   170 %\texttt{distinct} &
   171 %\texttt{files} &
   172 %\texttt{in} &
   173 %\texttt{induction} &
   174 %\texttt{infixl} \\
   175 %\texttt{infixr} &
   176 %\texttt{inject} &
   177 %\texttt{intrs} &
   178 %\texttt{is} &
   179 %\texttt{monos} \\
   180 %\texttt{output} &
   181 %\texttt{where} &
   182 % &
   183 % &
   184 % \\
   185 %\hline
   186 %\end{tabular}
   187 %\end{center}
   188 %\caption{Minor Keywords in HOL Theories}
   189 %\label{tab:keywords}
   190 %\end{table}