8 \begin{tabular}{|l|l|l|}
10 \indexboldpos{\isasymlbrakk}{$Isabrl} &
11 \texttt{[|}\index{$Isabrl@\ttlbr|bold} &
13 \indexboldpos{\isasymrbrakk}{$Isabrr} &
14 \texttt{|]}\index{$Isabrr@\ttrbr|bold} &
16 \indexboldpos{\isasymImp}{$IsaImp} &
17 \ttindexboldpos{==>}{$IsaImp} &
18 \verb$\<Longrightarrow>$ \\
19 \isasymAnd\index{$IsaAnd@\isasymAnd|bold}&
20 \texttt{!!}\index{$IsaAnd@\ttAnd|bold} &
22 \indexboldpos{\isasymequiv}{$IsaEq} &
23 \ttindexboldpos{==}{$IsaEq} &
25 \indexboldpos{\isasymlambda}{$Isalam} &
26 \texttt{\%}\indexbold{$Isalam@\texttt{\%}} &
28 \indexboldpos{\isasymFun}{$IsaFun} &
29 \ttindexboldpos{=>}{$IsaFun} &
30 \verb$\<Rightarrow>$ \\
31 \indexboldpos{\isasymand}{$HOL0and} &
32 \texttt{\&}\indexbold{$HOL0and@{\texttt{\&}}} &
34 \indexboldpos{\isasymor}{$HOL0or} &
35 \texttt{|}\index{$HOL0or@\ttor|bold} &
37 \indexboldpos{\isasymimp}{$HOL0imp} &
38 \ttindexboldpos{-->}{$HOL0imp} &
39 \verb$\<longrightarrow>$ \\
40 \indexboldpos{\isasymnot}{$HOL0not} &
41 \verb$~$\index{$HOL0not@\verb$~$|bold} &
43 \indexboldpos{\isasymnoteq}{$HOL0noteq} &
44 \verb$~=$\index{$HOL0noteq@\verb$~=$|bold} &
46 \indexboldpos{\isasymforall}{$HOL0All} &
47 \ttindexbold{ALL}, \texttt{!}\index{$HOL0All@\ttall|bold} &
49 \indexboldpos{\isasymexists}{$HOL0Ex} &
50 \ttindexbold{EX}, \texttt{?}\index{$HOL0Ex@\texttt{?}|bold} &
52 \isasymuniqex\index{$HOL0ExU@\isasymuniqex|bold} &
53 \ttEXU\index{EXX@\ttEXU|bold}, \ttuniquex\index{$HOL0ExU@\ttuniquex|bold} &
55 \indexboldpos{\isasymepsilon}{$HOL0ExSome} &
58 \indexboldpos{\isasymcirc}{$HOL1} &
61 \indexboldpos{\isasymle}{$HOL2arithrel}&
62 \ttindexboldpos{<=}{$HOL2arithrel}&
64 \indexboldpos{\isasymtimes}{$IsaFun}&
65 \ttindexboldpos{*}{$HOL2arithfun} &
67 \indexboldpos{\isasymin}{$HOL3Set0a}&
68 \ttindexboldpos{:}{$HOL3Set0b} &
70 \isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} &
71 \verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} &
73 \indexboldpos{\isasymsubseteq}{$HOL3Set0e}&
74 \verb$<=$ & \verb$\<subseteq>$\\
75 \indexboldpos{\isasymsubset}{$HOL3Set0f}&
76 \verb$<$ & \verb$\<subset>$\\
77 \indexboldpos{\isasymunion}{$HOL3Set1}&
80 \indexboldpos{\isasyminter}{$HOL3Set1}&
83 \isasymUnion\index{$HOL3Set2@\isasymUnion|bold}&
84 \ttindexbold{UN}, \ttindexbold{Union} &
86 \isasymInter\index{$HOL3Set2@\isasymInter|bold}&
87 \ttindexbold{INT}, \ttindexbold{Inter} &
92 \caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes}
94 \end{figure}\indexbold{ASCII symbols}
99 \begin{tabular}{|lllll|}
127 \caption{Reserved words in HOL terms}
128 \label{fig:ReservedWords}
132 %\begin{figure}[htbp]
134 %\begin{tabular}{|lllll|}
144 %\texttt{induction} &
159 %\caption{Minor keywords in HOL theories}
160 %\label{fig:keywords}