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{\isasymbar~\isasymbar}{$HOL2arithfun}&
63 \verb$\<bar> \<bar>$\\
64 \indexboldpos{\isasymle}{$HOL2arithrel}&
65 \ttindexboldpos{<=}{$HOL2arithrel}&
67 \indexboldpos{\isasymtimes}{$Isatype}&
68 \ttindexboldpos{*}{$HOL2arithfun} &
70 \indexboldpos{\isasymin}{$HOL3Set0a}&
71 \ttindexboldpos{:}{$HOL3Set0b} &
73 \isasymnotin\index{$HOL3Set0c@\isasymnotin|bold} &
74 \verb$~:$\index{$HOL3Set0d@\verb$~:$|bold} &
76 \indexboldpos{\isasymsubseteq}{$HOL3Set0e}&
77 \verb$<=$ & \verb$\<subseteq>$\\
78 \indexboldpos{\isasymsubset}{$HOL3Set0f}&
79 \verb$<$ & \verb$\<subset>$\\
80 \indexboldpos{\isasymunion}{$HOL3Set1}&
83 \indexboldpos{\isasyminter}{$HOL3Set1}&
86 \isasymUnion\index{$HOL3Set2@\isasymUnion|bold}&
87 \ttindexbold{UN}, \ttindexbold{Union} &
89 \isasymInter\index{$HOL3Set2@\isasymInter|bold}&
90 \ttindexbold{INT}, \ttindexbold{Inter} &
92 \isactrlsup{\isacharasterisk}\index{$HOL4star@\isactrlsup{\isacharasterisk}|bold}&
93 \verb$^*$\index{$HOL4star@\verb$^$\texttt{*}|bold} &
95 \isasyminverse\index{$HOL4inv@\isasyminverse|bold}&
96 \verb$^-1$\index{$HOL4inv@\verb$^-1$|bold} &
101 \caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes}
103 \end{figure}\indexbold{ASCII symbols}
107 \begin{tabular}{|lllllllll|}
145 \caption{Reserved words in HOL terms}
146 \label{fig:ReservedWords}
150 %\begin{figure}[htbp]
152 %\begin{tabular}{|lllll|}
162 %\texttt{induction} &
177 %\caption{Minor keywords in HOL theories}
178 %\label{fig:keywords}