doc-src/TutorialI/appendix.tex

 \hline
 \texttt{ALL} &
 \texttt{BIT} &
 \texttt{CHR} &
 \texttt{EX} &
-\texttt{GOAL} &
+\texttt{GREATEST} &
 \texttt{INT} &
 \texttt{Int} &
 \texttt{LEAST} &
 \texttt{O} \\
 \texttt{OFCLASS} &
 \texttt{PI} &
 \texttt{PROP} &
 \texttt{SIGMA} &
 \texttt{SOME} &
+\texttt{THE} &
 \texttt{TYPE} &
 \texttt{UN} &
-\texttt{Un} &\\
+\texttt{Un} \\
+\texttt{WRT} &
 \texttt{case} &
 \texttt{choose} &
 \texttt{div} &
 \texttt{dvd} &
 \texttt{else} &
 \texttt{funcset} &
 \texttt{if} &
-\texttt{in} &
-\texttt{lam} \\
+\texttt{in} \\
 \texttt{let} &
 \texttt{mem} &
 \texttt{mod} &
 \texttt{o} &
 \texttt{of} &
 \texttt{op} &
-\texttt{then}&&\\
+\texttt{then} &&\\
 \hline
 \end{tabular}
 \end{center}
 \caption{Reserved Words in HOL Terms}
 \label{tab:ReservedWords}