nipkow@8743: \appendix
nipkow@8743: 
nipkow@8743: \chapter{Appendix}
nipkow@8743: \label{sec:Appendix}
nipkow@8743: 
nipkow@10978: \begin{table}[htbp]
nipkow@8743: \begin{center}
nipkow@10171: \begin{tabular}{|l|l|l|}
nipkow@8743: \hline
nipkow@10171: \indexboldpos{\isasymlbrakk}{$Isabrl} &
nipkow@10171: \texttt{[|}\index{$Isabrl@\ttlbr|bold} &
nipkow@10171: \verb$\<lbrakk>$ \\
nipkow@10171: \indexboldpos{\isasymrbrakk}{$Isabrr} &
nipkow@10171: \texttt{|]}\index{$Isabrr@\ttrbr|bold} &
nipkow@10171: \verb$\<rbrakk>$ \\
nipkow@10171: \indexboldpos{\isasymImp}{$IsaImp} &
nipkow@10171: \ttindexboldpos{==>}{$IsaImp} &
nipkow@10171: \verb$\<Longrightarrow>$ \\
nipkow@10328: \isasymAnd\index{$IsaAnd@\isasymAnd|bold}&
nipkow@10171: \texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
nipkow@10171: \verb$\<And>$ \\
nipkow@10171: \indexboldpos{\isasymequiv}{$IsaEq} &
nipkow@10171: \ttindexboldpos{==}{$IsaEq} &
nipkow@10171: \verb$\<equiv>$ \\
nipkow@11203: \indexboldpos{\isasymrightleftharpoons}{$IsaEqTrans} &
nipkow@11203: \ttindexboldpos{==}{$IsaEq} &
nipkow@11203: \verb$\<rightleftharpoons>$ \\
nipkow@11203: \indexboldpos{\isasymrightharpoonup}{$IsaEqTrans1} &
nipkow@11203: \ttindexboldpos{=>}{$IsaFun} &
nipkow@11203: \verb$\<rightharpoonup>$ \\
nipkow@11203: \indexboldpos{\isasymleftharpoondown}{$IsaEqTrans2} &
nipkow@11203: \ttindexboldpos{<=}{$IsaFun2} &
nipkow@11203: \verb$\<leftharpoondown>$ \\
nipkow@10171: \indexboldpos{\isasymlambda}{$Isalam} &
nipkow@10171: \texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
nipkow@10171: \verb$\<lambda>$ \\
nipkow@10171: \indexboldpos{\isasymFun}{$IsaFun} &
nipkow@10171: \ttindexboldpos{=>}{$IsaFun} &
nipkow@10171: \verb$\<Rightarrow>$ \\
nipkow@8743: \indexboldpos{\isasymand}{$HOL0and} &
nipkow@10171: \texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
nipkow@10171: \verb$\<and>$ \\
nipkow@8743: \indexboldpos{\isasymor}{$HOL0or} &
nipkow@10171: \texttt{|}\index{$HOL0or@\ttor|bold} &
nipkow@10171: \verb$\<or>$ \\
nipkow@8743: \indexboldpos{\isasymimp}{$HOL0imp} &
nipkow@10171: \ttindexboldpos{-->}{$HOL0imp} &
nipkow@10171: \verb$\<longrightarrow>$ \\
nipkow@8743: \indexboldpos{\isasymnot}{$HOL0not} &
nipkow@10171: \verb$~$\index{$HOL0not@\verb$~$|bold} &
nipkow@10171: \verb$\<not>$ \\
nipkow@8743: \indexboldpos{\isasymnoteq}{$HOL0noteq} &
nipkow@10171: \verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
nipkow@10171: \verb$\<noteq>$ \\
nipkow@8743: \indexboldpos{\isasymforall}{$HOL0All} &
nipkow@10171: \ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} &
nipkow@10171: \verb$\<forall>$ \\
nipkow@8743: \indexboldpos{\isasymexists}{$HOL0Ex} &
nipkow@10171: \ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
nipkow@10171: \verb$\<exists>$ \\
nipkow@8743: \isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
nipkow@10171: \ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
nipkow@10171: \verb$\<exists>!$\\
nipkow@10171: \indexboldpos{\isasymepsilon}{$HOL0ExSome} &
nipkow@15364: \ttindexbold{SOME}, \isa{\at}\index{$HOL2list@\isa{\at}} &
nipkow@10178: \verb$\<epsilon>$\\
nipkow@8743: \indexboldpos{\isasymcirc}{$HOL1} &
nipkow@10171: \ttindexbold{o} &
nipkow@10178: \verb$\<circ>$\\
nipkow@10590: \indexboldpos{\isasymbar~\isasymbar}{$HOL2arithfun}&
nipkow@10590: \ttindexbold{abs}&
nipkow@10590: \verb$\<bar> \<bar>$\\
nipkow@8743: \indexboldpos{\isasymle}{$HOL2arithrel}&
nipkow@15364: \isadxboldpos{<=}{$HOL2arithrel}&
nipkow@10171: \verb$\<le>$\\
nipkow@10538: \indexboldpos{\isasymtimes}{$Isatype}&
nipkow@9933: \ttindexboldpos{*}{$HOL2arithfun} &
nipkow@10171: \verb$\<times>$\\
nipkow@10242: \indexboldpos{\isasymin}{$HOL3Set0a}&
nipkow@10242: \ttindexboldpos{:}{$HOL3Set0b} &
nipkow@10171: \verb$\<in>$\\
nipkow@10242: \isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} &
nipkow@10242: \verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} &
nipkow@10171: \verb$\<notin>$\\
nipkow@10242: \indexboldpos{\isasymsubseteq}{$HOL3Set0e}&
nipkow@10242: \verb$<=$ & \verb$\<subseteq>$\\
nipkow@10242: \indexboldpos{\isasymsubset}{$HOL3Set0f}&
nipkow@10242: \verb$<$ & \verb$\<subset>$\\
nipkow@10242: \indexboldpos{\isasymunion}{$HOL3Set1}&
nipkow@10171: \ttindexbold{Un} &
nipkow@10171: \verb$\<union>$\\
nipkow@10242: \indexboldpos{\isasyminter}{$HOL3Set1}&
nipkow@10171: \ttindexbold{Int} &
nipkow@10171: \verb$\<inter>$\\
nipkow@10328: \isasymUnion\index{$HOL3Set2@\isasymUnion|bold}&
nipkow@10171: \ttindexbold{UN}, \ttindexbold{Union} &
nipkow@10171: \verb$\<Union>$\\
nipkow@10328: \isasymInter\index{$HOL3Set2@\isasymInter|bold}&
nipkow@10171: \ttindexbold{INT}, \ttindexbold{Inter} &
nipkow@10171: \verb$\<Inter>$\\
nipkow@10801: \isactrlsup{\isacharasterisk}\index{$HOL4star@\isactrlsup{\isacharasterisk}|bold}&
nipkow@10801: \verb$^*$\index{$HOL4star@\verb$^$\texttt{*}|bold} &
nipkow@10801: \verb$\<^sup>*$\\
nipkow@10801: \isasyminverse\index{$HOL4inv@\isasyminverse|bold}&
nipkow@10801: \verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} &
nipkow@10801: \verb$\<inverse>$\\
nipkow@8743: \hline
nipkow@8743: \end{tabular}
nipkow@8743: \end{center}
paulson@11450: \caption{Mathematical Symbols, Their \textsc{ascii}-Equivalents and Internal Names}
nipkow@10978: \label{tab:ascii}
nipkow@10983: \end{table}\indexbold{ASCII@\textsc{ascii} symbols}
nipkow@8743: 
nipkow@10978: \input{Misc/document/appendix.tex}
nipkow@10978: 
nipkow@10978: \begin{table}[htbp]
nipkow@8743: \begin{center}
nipkow@12489: \begin{tabular}{@{}|lllllllll|@{}}
nipkow@8743: \hline
nipkow@8743: \texttt{ALL} &
nipkow@10654: \texttt{BIT} &
nipkow@10654: \texttt{CHR} &
nipkow@10654: \texttt{EX} &
wenzelm@12458: \texttt{GREATEST} &
nipkow@10654: \texttt{INT} &
nipkow@10654: \texttt{Int} &
nipkow@10654: \texttt{LEAST} &
nipkow@10654: \texttt{O} \\
nipkow@10654: \texttt{OFCLASS} &
nipkow@10654: \texttt{PI} &
nipkow@10654: \texttt{PROP} &
nipkow@10654: \texttt{SIGMA} &
nipkow@10654: \texttt{SOME} &
wenzelm@12458: \texttt{THE} &
nipkow@10654: \texttt{TYPE} &
nipkow@10654: \texttt{UN} &
wenzelm@12458: \texttt{Un} \\
wenzelm@12458: \texttt{WRT} &
nipkow@8743: \texttt{case} &
nipkow@10654: \texttt{choose} &
nipkow@8743: \texttt{div} &
nipkow@8743: \texttt{dvd} &
nipkow@10654: \texttt{else} &
nipkow@10654: \texttt{funcset} &
nipkow@8743: \texttt{if} &
wenzelm@12458: \texttt{in} \\
nipkow@8743: \texttt{let} &
nipkow@10654: \texttt{mem} &
nipkow@8743: \texttt{mod} &
nipkow@10654: \texttt{o} &
nipkow@8743: \texttt{of} &
nipkow@8743: \texttt{op} &
wenzelm@12458: \texttt{then} &&\\
nipkow@8743: \hline
nipkow@8743: \end{tabular}
nipkow@8743: \end{center}
paulson@11450: \caption{Reserved Words in HOL Terms}
nipkow@10978: \label{tab:ReservedWords}
nipkow@10978: \end{table}
wenzelm@8845: 
wenzelm@8845: 
nipkow@10978: %\begin{table}[htbp]
nipkow@9541: %\begin{center}
nipkow@9541: %\begin{tabular}{|lllll|}
nipkow@9541: %\hline
nipkow@9541: %\texttt{and} &
nipkow@9541: %\texttt{binder} &
nipkow@9541: %\texttt{concl} &
nipkow@9541: %\texttt{congs} \\
nipkow@9541: %\texttt{distinct} &
nipkow@9541: %\texttt{files} &
nipkow@9541: %\texttt{in} &
nipkow@9541: %\texttt{induction} &
nipkow@9541: %\texttt{infixl} \\
nipkow@9541: %\texttt{infixr} &
nipkow@9541: %\texttt{inject} &
nipkow@9541: %\texttt{intrs} &
nipkow@9541: %\texttt{is} &
nipkow@9541: %\texttt{monos} \\
nipkow@9541: %\texttt{output} &
nipkow@9541: %\texttt{where} &
nipkow@9541: % &
nipkow@9541: % &
nipkow@9541: % \\
nipkow@9541: %\hline
nipkow@9541: %\end{tabular}
nipkow@9541: %\end{center}
paulson@11450: %\caption{Minor Keywords in HOL Theories}
nipkow@10978: %\label{tab:keywords}
nipkow@10978: %\end{table}