21 \item {\tt\%}, \bold{3} |
21 \item {\tt\%}, \bold{3} |
22 \item {\tt =>}, \bold{2} |
22 \item {\tt =>}, \bold{2} |
23 |
23 |
24 \indexspace |
24 \indexspace |
25 |
25 |
26 \item {\tt addsimps}, \bold{21} |
26 \item {\tt addsimps}, \bold{22} |
27 \item {\tt Addsplits}, \bold{23} |
27 \item {\tt Addsplits}, \bold{24} |
28 \item {\tt addsplits}, \bold{23} |
28 \item {\tt addsplits}, \bold{24} |
29 \item {\tt and}, \bold{28} |
29 \item {\tt and}, \bold{29} |
30 \item {\tt Asm_full_simp_tac}, \bold{20} |
30 \item {\tt Asm_full_simp_tac}, \bold{21} |
31 \item {\tt asm_full_simp_tac}, \bold{21} |
31 \item {\tt asm_full_simp_tac}, \bold{22} |
32 \item {\tt Asm_simp_tac}, \bold{20} |
32 \item {\tt Asm_simp_tac}, \bold{21} |
33 \item {\tt asm_simp_tac}, \bold{21} |
33 \item {\tt asm_simp_tac}, \bold{22} |
34 |
34 |
35 \indexspace |
35 \indexspace |
36 |
36 |
37 \item {\tt bool}, 2 |
37 \item {\tt bool}, 2 |
38 |
38 |
39 \indexspace |
39 \indexspace |
40 |
40 |
41 \item {\tt case}, \bold{3}, 4, \bold{13}, 23 |
41 \item {\tt case}, \bold{3}, 4, \bold{13}, 24 |
42 \item {\tt constdefs}, \bold{18} |
42 \item {\tt constdefs}, \bold{18} |
43 \item {\tt consts}, \bold{7} |
43 \item {\tt consts}, \bold{7} |
44 \item {\tt context}, \bold{11} |
44 \item {\tt context}, \bold{11} |
45 \item current theory, \bold{11} |
45 \item current theory, \bold{11} |
46 |
46 |
47 \indexspace |
47 \indexspace |
48 |
48 |
49 \item {\tt datatype}, \bold{7}, 28--32 |
49 \item {\tt datatype}, \bold{7}, 29--33 |
50 \item {\tt defs}, \bold{18} |
50 \item {\tt defs}, \bold{18} |
51 \item {\tt delsimps}, \bold{21} |
51 \item {\tt delsimps}, \bold{22} |
52 \item {\tt Delsplits}, \bold{23} |
52 \item {\tt Delsplits}, \bold{24} |
53 \item {\tt delsplits}, \bold{23} |
53 \item {\tt delsplits}, \bold{24} |
54 \item {\tt div}, \bold{17} |
54 \item {\tt div}, \bold{17} |
55 |
55 |
56 \indexspace |
56 \indexspace |
57 |
57 |
58 \item {\tt exhaust_tac}, \bold{14} |
58 \item {\tt exhaust_tac}, \bold{14} |
59 |
59 |
60 \indexspace |
60 \indexspace |
61 |
61 |
62 \item {\tt False}, \bold{3} |
62 \item {\tt False}, \bold{3} |
63 \item formula, \bold{3} |
63 \item formula, \bold{3} |
64 \item {\tt Full_simp_tac}, \bold{20} |
64 \item {\tt Full_simp_tac}, \bold{21} |
65 \item {\tt full_simp_tac}, \bold{21} |
65 \item {\tt full_simp_tac}, \bold{22} |
66 |
66 |
67 \indexspace |
67 \indexspace |
68 |
68 |
69 \item {\tt hd}, \bold{12} |
69 \item {\tt hd}, \bold{12} |
70 |
70 |
71 \indexspace |
71 \indexspace |
72 |
72 |
73 \item {\tt if}, \bold{3}, 4, 23 |
73 \item {\tt if}, \bold{3}, 4, 24 |
74 \item {\tt infixr}, \bold{7} |
74 \item {\tt infixr}, \bold{7} |
75 \item inner syntax, \bold{8} |
75 \item inner syntax, \bold{8} |
76 |
76 |
77 \indexspace |
77 \indexspace |
78 |
78 |
79 \item {\tt LEAST}, \bold{17} |
79 \item {\tt LEAST}, \bold{17} |
80 \item {\tt let}, \bold{3}, 4, 22 |
80 \item {\tt let}, \bold{3}, 4, 23 |
81 \item {\tt list}, 2 |
81 \item {\tt list}, 2 |
82 \item loading theories, 12 |
82 \item loading theories, 12 |
83 |
83 |
84 \indexspace |
84 \indexspace |
85 |
85 |
86 \item {\tt Main}, \bold{2} |
86 \item {\tt Main}, \bold{2} |
87 \item measure function, \bold{35} |
87 \item measure function, \bold{35} |
88 \item {\tt mod}, \bold{17} |
88 \item {\tt mod}, \bold{17} |
89 \item {\tt mutual_induct_tac}, \bold{29} |
89 \item {\tt mutual_induct_tac}, \bold{30} |
90 |
90 |
91 \indexspace |
91 \indexspace |
92 |
92 |
93 \item {\tt nat}, 2, \bold{16} |
93 \item {\tt nat}, 2, \bold{17} |
94 \item {\tt None}, \bold{32} |
94 \item {\tt None}, \bold{33} |
95 |
95 |
96 \indexspace |
96 \indexspace |
97 |
97 |
98 \item {\tt option}, \bold{32} |
98 \item {\tt option}, \bold{33} |
99 |
99 |
100 \indexspace |
100 \indexspace |
101 |
101 |
102 \item parent theory, \bold{1} |
102 \item parent theory, \bold{1} |
103 \item primitive recursion, \bold{13} |
103 \item primitive recursion, \bold{13} |
104 \item {\tt primrec}, 7, \bold{13}, 28--32 |
104 \item {\tt primrec}, 7, \bold{13}, 29--33 |
105 \item proof scripts, \bold{2} |
105 \item proof scripts, \bold{2} |
106 |
106 |
107 \indexspace |
107 \indexspace |
108 |
108 |
109 \item {\tt recdef}, 34--37 |
109 \item {\tt recdef}, 35--38 |
110 \item reloading theories, 12 |
110 \item reloading theories, 12 |
111 |
111 |
112 \indexspace |
112 \indexspace |
113 |
113 |
114 \item schematic variable, \bold{4} |
114 \item schematic variable, \bold{4} |
115 \item {\tt set}, 2 |
115 \item {\tt set}, 2 |
116 \item {\tt show_brackets}, \bold{4} |
116 \item {\tt show_brackets}, \bold{4} |
117 \item {\tt show_types}, \bold{3}, 11 |
117 \item {\tt show_types}, \bold{3}, 11 |
118 \item {\tt Simp_tac}, \bold{20} |
118 \item {\tt Simp_tac}, \bold{21} |
119 \item {\tt simp_tac}, \bold{21} |
119 \item {\tt simp_tac}, \bold{22} |
120 \item simplifier, \bold{19} |
120 \item simplifier, \bold{20} |
121 \item simpset, \bold{20} |
121 \item simpset, \bold{21} |
122 \item {\tt Some}, \bold{32} |
122 \item {\tt Some}, \bold{33} |
123 |
123 |
124 \indexspace |
124 \indexspace |
125 |
125 |
126 \item tactic, \bold{11} |
126 \item tactic, \bold{11} |
127 \item term, \bold{3} |
127 \item term, \bold{3} |
128 \item theory, \bold{1} |
128 \item theory, \bold{1} |
129 \item {\tt tl}, \bold{12} |
129 \item {\tt tl}, \bold{12} |
130 \item total, \bold{7} |
130 \item total, \bold{7} |
131 \item tracing the simplifier, \bold{24} |
131 \item tracing the simplifier, \bold{25} |
132 \item {\tt True}, \bold{3} |
132 \item {\tt True}, \bold{3} |
133 \item type constraints, \bold{3} |
133 \item type constraints, \bold{3} |
134 \item type inference, \bold{3} |
134 \item type inference, \bold{3} |
135 \item type synonyms, \bold{18} |
135 \item type synonyms, \bold{18} |
136 \item {\tt types}, \bold{18} |
136 \item {\tt types}, \bold{18} |