3 \item {\tt[]}, \bold{7}
4 \item {\tt\#}, \bold{7}
5 \item {\ttnot}, \bold{3}
6 \item {\tt-->}, \bold{3}
7 \item {\tt\&}, \bold{3}
8 \item {\ttor}, \bold{3}
9 \item {\tt?}, \bold{3}, 4
10 \item {\ttall}, \bold{3}
11 \item {\ttuniquex}, \bold{3}
12 \item {\tt *}, \bold{17}
13 \item {\tt +}, \bold{17}
14 \item {\tt -}, \bold{17}
15 \item {\tt <}, \bold{17}
16 \item {\tt <=}, \bold{17}
17 \item \ttlbr, \bold{9}
18 \item \ttrbr, \bold{9}
19 \item {\tt==>}, \bold{9}
20 \item {\tt==}, \bold{18}
21 \item {\tt\%}, \bold{3}
22 \item {\tt =>}, \bold{2}
26 \item {\tt addsimps}, \bold{22}
27 \item {\tt Addsplits}, \bold{24}
28 \item {\tt addsplits}, \bold{24}
29 \item {\tt Asm_full_simp_tac}, \bold{21}
30 \item {\tt asm_full_simp_tac}, \bold{22}
31 \item {\tt Asm_simp_tac}, \bold{21}
32 \item {\tt asm_simp_tac}, \bold{22}
40 \item {\tt case}, \bold{3}, 4, \bold{13}, 24
41 \item {\tt constdefs}, \bold{18}
42 \item {\tt consts}, \bold{7}
43 \item {\tt context}, \bold{11}
44 \item current theory, \bold{11}
48 \item {\tt datatype}, \bold{7}
49 \item {\tt defs}, \bold{18}
50 \item {\tt delsimps}, \bold{22}
51 \item {\tt Delsplits}, \bold{24}
52 \item {\tt delsplits}, \bold{24}
53 \item {\tt div}, \bold{17}
57 \item {\tt exhaust_tac}, \bold{14}
61 \item {\tt False}, \bold{3}
62 \item formula, \bold{3}
63 \item {\tt Full_simp_tac}, \bold{21}
64 \item {\tt full_simp_tac}, \bold{22}
68 \item {\tt hd}, \bold{12}
72 \item {\tt if}, \bold{3}, 4, 24
73 \item {\tt infixr}, \bold{7}
74 \item inner syntax, \bold{8}
78 \item {\tt LEAST}, \bold{17}
79 \item {\tt let}, \bold{3}, 4, 23
81 \item loading theories, 12
85 \item {\tt Main}, \bold{2}
86 \item measure function, \bold{29}
87 \item {\tt mod}, \bold{17}
91 \item {\tt nat}, 2, \bold{17}
95 \item parent theory, \bold{1}
96 \item primitive recursion, \bold{13}
97 \item proof scripts, \bold{2}
101 \item {\tt recdef}, 29--31
102 \item reloading theories, 12
106 \item schematic variable, \bold{4}
108 \item {\tt show_brackets}, \bold{4}
109 \item {\tt show_types}, \bold{3}, 11
110 \item {\tt Simp_tac}, \bold{21}
111 \item {\tt simp_tac}, \bold{22}
112 \item simplifier, \bold{20}
113 \item simpset, \bold{21}
117 \item tactic, \bold{11}
119 \item theory, \bold{1}
120 \item {\tt tl}, \bold{12}
121 \item total, \bold{7}
122 \item tracing the simplifier, \bold{25}
123 \item {\tt True}, \bold{3}
124 \item type constraints, \bold{3}
125 \item type inference, \bold{3}
126 \item type synonyms, \bold{18}
127 \item {\tt types}, \bold{18}
131 \item unknown, \bold{4}
132 \item {\tt update}, \bold{12}
133 \item {\tt use_thy}, \bold{2}, 12