\begin{theindex}
\item {\tt[]}, \bold{7}
\item {\tt\#}, \bold{7}
\item {\ttnot}, \bold{3}
\item {\tt-->}, \bold{3}
\item {\tt\&}, \bold{3}
\item {\ttor}, \bold{3}
\item {\tt?}, \bold{3}, 4
\item {\ttall}, \bold{3}
\item {\ttuniquex}, \bold{3}
\item {\tt *}, \bold{17}
\item {\tt +}, \bold{17}
\item {\tt -}, \bold{17}
\item {\tt <}, \bold{17}
\item {\tt <=}, \bold{17}
\item \ttlbr, \bold{9}
\item \ttrbr, \bold{9}
\item {\tt==>}, \bold{9}
\item {\tt==}, \bold{18}
\item {\tt\%}, \bold{3}
\item {\tt =>}, \bold{2}
\indexspace
\item {\tt addsimps}, \bold{22}
\item {\tt Addsplits}, \bold{24}
\item {\tt addsplits}, \bold{24}
\item {\tt Asm_full_simp_tac}, \bold{21}
\item {\tt asm_full_simp_tac}, \bold{22}
\item {\tt Asm_simp_tac}, \bold{21}
\item {\tt asm_simp_tac}, \bold{22}
\indexspace
\item {\tt bool}, 2
\indexspace
\item {\tt case}, \bold{3}, 4, \bold{13}, 24
\item {\tt constdefs}, \bold{18}
\item {\tt consts}, \bold{7}
\item {\tt context}, \bold{11}
\item current theory, \bold{11}
\indexspace
\item {\tt datatype}, \bold{7}
\item {\tt defs}, \bold{18}
\item {\tt delsimps}, \bold{22}
\item {\tt Delsplits}, \bold{24}
\item {\tt delsplits}, \bold{24}
\item {\tt div}, \bold{17}
\indexspace
\item {\tt exhaust_tac}, \bold{14}
\indexspace
\item {\tt False}, \bold{3}
\item formula, \bold{3}
\item {\tt Full_simp_tac}, \bold{21}
\item {\tt full_simp_tac}, \bold{22}
\indexspace
\item {\tt hd}, \bold{12}
\indexspace
\item {\tt if}, \bold{3}, 4, 24
\item {\tt infixr}, \bold{7}
\item inner syntax, \bold{8}
\indexspace
\item {\tt LEAST}, \bold{17}
\item {\tt let}, \bold{3}, 4, 23
\item {\tt list}, 2
\item loading theories, 12
\indexspace
\item {\tt Main}, \bold{2}
\item measure function, \bold{29}
\item {\tt mod}, \bold{17}
\indexspace
\item {\tt nat}, 2, \bold{17}
\indexspace
\item parent theory, \bold{1}
\item primitive recursion, \bold{13}
\item proof scripts, \bold{2}
\indexspace
\item {\tt recdef}, 29--31
\item reloading theories, 12
\indexspace
\item schematic variable, \bold{4}
\item {\tt set}, 2
\item {\tt show_brackets}, \bold{4}
\item {\tt show_types}, \bold{3}, 11
\item {\tt Simp_tac}, \bold{21}
\item {\tt simp_tac}, \bold{22}
\item simplifier, \bold{20}
\item simpset, \bold{21}
\indexspace
\item tactic, \bold{11}
\item term, \bold{3}
\item theory, \bold{1}
\item {\tt tl}, \bold{12}
\item total, \bold{7}
\item tracing the simplifier, \bold{25}
\item {\tt True}, \bold{3}
\item type constraints, \bold{3}
\item type inference, \bold{3}
\item type synonyms, \bold{18}
\item {\tt types}, \bold{18}
\indexspace
\item unknown, \bold{4}
\item {\tt update}, \bold{12}
\item {\tt use_thy}, \bold{2}, 12
\end{theindex}