1.1 --- a/doc-src/TutorialI/appendix.tex	Mon Oct 09 09:33:45 2000 +0200
     1.2 +++ b/doc-src/TutorialI/appendix.tex	Mon Oct 09 10:18:21 2000 +0200
     1.3 @@ -5,80 +5,90 @@
     1.4  
     1.5  \begin{figure}[htbp]
     1.6  \begin{center}
     1.7 -\begin{tabular}{|ccccccccccc|}
     1.8 +\begin{tabular}{|l|l|l|}
     1.9  \hline
    1.10 +\indexboldpos{\isasymlbrakk}{$Isabrl} &
    1.11 +\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
    1.12 +\verb$\<lbrakk>$ \\
    1.13 +\indexboldpos{\isasymrbrakk}{$Isabrr} &
    1.14 +\texttt{|]}\index{$Isabrr@\ttrbr|bold} &
    1.15 +\verb$\<rbrakk>$ \\
    1.16 +\indexboldpos{\isasymImp}{$IsaImp} &
    1.17 +\ttindexboldpos{==>}{$IsaImp} &
    1.18 +\verb$\<Longrightarrow>$ \\
    1.19 +\indexboldpos{\isasymAnd}{$IsaAnd} &
    1.20 +\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
    1.21 +\verb$\<And>$ \\
    1.22 +\indexboldpos{\isasymequiv}{$IsaEq} &
    1.23 +\ttindexboldpos{==}{$IsaEq} &
    1.24 +\verb$\<equiv>$ \\
    1.25 +\indexboldpos{\isasymlambda}{$Isalam} &
    1.26 +\texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
    1.27 +\verb$\<lambda>$ \\
    1.28 +\indexboldpos{\isasymFun}{$IsaFun} &
    1.29 +\ttindexboldpos{=>}{$IsaFun} &
    1.30 +\verb$\<Rightarrow>$ \\
    1.31  \indexboldpos{\isasymand}{$HOL0and} &
    1.32 +\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
    1.33 +\verb$\<and>$ \\
    1.34  \indexboldpos{\isasymor}{$HOL0or} &
    1.35 +\texttt{|}\index{$HOL0or@\ttor|bold} &
    1.36 +\verb$\<or>$ \\
    1.37  \indexboldpos{\isasymimp}{$HOL0imp} &
    1.38 +\ttindexboldpos{-->}{$HOL0imp} &
    1.39 +\verb$\<longrightarrow>$ \\
    1.40  \indexboldpos{\isasymnot}{$HOL0not} &
    1.41 +\verb$~$\index{$HOL0not@\verb$~$|bold} &
    1.42 +\verb$\<not>$ \\
    1.43  \indexboldpos{\isasymnoteq}{$HOL0noteq} &
    1.44 +\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
    1.45 +\verb$\<noteq>$ \\
    1.46  \indexboldpos{\isasymforall}{$HOL0All} &
    1.47 -\isasymforall &
    1.48 +\ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} &
    1.49 +\verb$\<forall>$ \\
    1.50  \indexboldpos{\isasymexists}{$HOL0Ex} &
    1.51 -\isasymexists &
    1.52 +\ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
    1.53 +\verb$\<exists>$ \\
    1.54  \isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
    1.55 -\isasymuniqex \\
    1.56 -\texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
    1.57 -\texttt{|}\index{$HOL0or@\ttor|bold} &
    1.58 -\ttindexboldpos{-->}{$HOL0imp} &
    1.59 -\verb$~$\index{$HOL0not@\verb$~$|bold} &
    1.60 -\verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
    1.61 -\ttindexbold{ALL} &
    1.62 -\texttt{!}\index{$HOL0All@\ttall|bold} &
    1.63 -\ttindexbold{EX} &
    1.64 -\texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
    1.65 -\ttEXU\index{EXX@\ttEXU|bold} &
    1.66 -\ttuniquex\index{$HOL0ExU@\ttuniquex|bold}\\
    1.67 -\hline\hline
    1.68 -\indexboldpos{\isasymlbrakk}{$Isabrl} &
    1.69 -\indexboldpos{\isasymrbrakk}{$Isabrr} &
    1.70 -\indexboldpos{\isasymImp}{$IsaImp} &
    1.71 -\indexboldpos{\isasymAnd}{$IsaAnd} &
    1.72 -\indexboldpos{\isasymequiv}{$IsaEq} &
    1.73 -\indexboldpos{\isasymlambda}{$Isalam} &
    1.74 -\indexboldpos{\isasymFun}{$IsaFun}&
    1.75 -&
    1.76 -&
    1.77 -&
    1.78 -\\
    1.79 -\texttt{[|}\index{$Isabrl@\ttlbr|bold} &
    1.80 -\texttt{|]}\index{$Isabrr@\ttrbr|bold} &
    1.81 -\ttindexboldpos{==>}{$IsaImp} &
    1.82 -\texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
    1.83 -\ttindexboldpos{==}{$IsaEq} &
    1.84 -\texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
    1.85 -\ttindexboldpos{=>}{$IsaFun}&
    1.86 -&
    1.87 -&
    1.88 -&
    1.89 - \\
    1.90 -\hline\hline
    1.91 +\ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
    1.92 +\verb$\<exists>!$\\
    1.93 +\indexboldpos{\isasymepsilon}{$HOL0ExSome} &
    1.94 +\ttindexbold{SOME} &
    1.95 +\verb$\<?>$\\
    1.96  \indexboldpos{\isasymcirc}{$HOL1} &
    1.97 +\ttindexbold{o} &
    1.98 +\verb$\<?>$\\
    1.99  \indexboldpos{\isasymle}{$HOL2arithrel}&
   1.100 +\ttindexboldpos{<=}{$HOL2arithrel}&
   1.101 +\verb$\<le>$\\
   1.102  \indexboldpos{\isasymtimes}{$IsaFun}&
   1.103 -&
   1.104 -&
   1.105 -&
   1.106 -&
   1.107 -&
   1.108 -&
   1.109 -&
   1.110 - \\
   1.111 -\ttindexbold{o} &
   1.112 -\ttindexboldpos{<=}{$HOL2arithrel}&
   1.113  \ttindexboldpos{*}{$HOL2arithfun} &
   1.114 -&
   1.115 -&
   1.116 -&
   1.117 -&
   1.118 -&
   1.119 -&
   1.120 -&
   1.121 -\\
   1.122 +\verb$\<times>$\\
   1.123 +\indexboldpos{\isasymin}{$HOL3Set}&
   1.124 +\ttindexboldpos{:}{$HOL3Set} &
   1.125 +\verb$\<in>$\\
   1.126 +? & %\indexboldpos{\isasymnotin}{$HOL3Set} fails for some strange reason
   1.127 +\verb$~:$\index{$HOL3Set@\verb$~:$|bold} &
   1.128 +\verb$\<notin>$\\
   1.129 +\indexboldpos{\isasymsubseteq}{$HOL3Set}&
   1.130 +\verb$<=$ &
   1.131 +\verb$\<subseteq>$\\
   1.132 +\indexboldpos{\isasymunion}{$HOL3Set}&
   1.133 +\ttindexbold{Un} &
   1.134 +\verb$\<union>$\\
   1.135 +\indexboldpos{\isasyminter}{$HOL3Set}&
   1.136 +\ttindexbold{Int} &
   1.137 +\verb$\<inter>$\\
   1.138 +\indexboldpos{\isasymUnion}{$HOL3Set}&
   1.139 +\ttindexbold{UN}, \ttindexbold{Union} &
   1.140 +\verb$\<Union>$\\
   1.141 +\indexboldpos{\isasymInter}{$HOL3Set}&
   1.142 +\ttindexbold{INT}, \ttindexbold{Inter} &
   1.143 +\verb$\<Inter>$\\
   1.144  \hline
   1.145  \end{tabular}
   1.146  \end{center}
   1.147 -\caption{Mathematical symbols and their ASCII-equivalents}
   1.148 +\caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes}
   1.149  \label{fig:ascii}
   1.150  \end{figure}\indexbold{ASCII symbols}
   1.151