equal
deleted
inserted
replaced
94 \end{center} |
94 \end{center} |
95 \caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes} |
95 \caption{Mathematical symbols, their ASCII-equivalents and ProofGeneral codes} |
96 \label{fig:ascii} |
96 \label{fig:ascii} |
97 \end{figure}\indexbold{ASCII symbols} |
97 \end{figure}\indexbold{ASCII symbols} |
98 |
98 |
99 |
|
100 \begin{figure}[htbp] |
99 \begin{figure}[htbp] |
101 \begin{center} |
100 \begin{center} |
102 \begin{tabular}{|lllll|} |
101 \begin{tabular}{|lllllllll|} |
103 \hline |
102 \hline |
104 \texttt{ALL} & |
103 \texttt{ALL} & |
|
104 \texttt{BIT} & |
|
105 \texttt{CHR} & |
|
106 \texttt{EX} & |
|
107 \texttt{GOAL} & |
|
108 \texttt{INT} & |
|
109 \texttt{Int} & |
|
110 \texttt{LEAST} & |
|
111 \texttt{O} \\ |
|
112 \texttt{OFCLASS} & |
|
113 \texttt{PI} & |
|
114 \texttt{PROP} & |
|
115 \texttt{SIGMA} & |
|
116 \texttt{SOME} & |
|
117 \texttt{TYPE} & |
|
118 \texttt{UN} & |
|
119 \texttt{Un} &\\ |
105 \texttt{case} & |
120 \texttt{case} & |
|
121 \texttt{choose} & |
106 \texttt{div} & |
122 \texttt{div} & |
107 \texttt{dvd} & |
123 \texttt{dvd} & |
108 \texttt{else} \\ |
124 \texttt{else} & |
109 \texttt{EX} & |
125 \texttt{funcset} & |
110 \texttt{if} & |
126 \texttt{if} & |
111 \texttt{in} & |
127 \texttt{in} & |
112 \texttt{INT} & |
128 \texttt{lam} \\ |
113 \texttt{Int} \\ |
|
114 \texttt{LEAST} & |
|
115 \texttt{let} & |
129 \texttt{let} & |
|
130 \texttt{mem} & |
116 \texttt{mod} & |
131 \texttt{mod} & |
117 \texttt{O} & |
132 \texttt{o} & |
118 \texttt{o} \\ |
|
119 \texttt{of} & |
133 \texttt{of} & |
120 \texttt{op} & |
134 \texttt{op} & |
121 \texttt{PROP} & |
135 \texttt{then}&&\\ |
122 \texttt{SIGMA} & |
|
123 \texttt{then} \\ |
|
124 \texttt{Times} & |
|
125 \texttt{UN} & |
|
126 \texttt{Un} &&\\ |
|
127 \hline |
136 \hline |
128 \end{tabular} |
137 \end{tabular} |
129 \end{center} |
138 \end{center} |
130 \caption{Reserved words in HOL terms} |
139 \caption{Reserved words in HOL terms} |
131 \label{fig:ReservedWords} |
140 \label{fig:ReservedWords} |