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

     1 \appendix

     3 \chapter{Appendix}

     4 \label{sec:Appendix}

     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}

   114 \input{Misc/document/appendix.tex}

   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}

   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}

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 15364	0c3891c3528f
child 49537	708278fc2dff
permissions	-rw-r--r--