1 \begin{theindex} |
1 \begin{theindex} |
2 |
2 |
3 \item {\tt !!} symbol, 68 |
3 \item {\tt !!} symbol, 69 |
4 \subitem in main goal, 8 |
4 \subitem in main goal, 8 |
5 \item {\tt\$}, \bold{60}, 85 |
5 \item {\tt\$}, \bold{60}, 86 |
6 \item {\tt\%} symbol, 68 |
6 \item {\tt\%} symbol, 69 |
7 \item * |
7 \item * |
8 \subitem claset, 136 |
8 \subitem claset, 137 |
9 \item {\tt ::} symbol, 68, 69 |
9 \item {\tt ::} symbol, 69, 70 |
10 \item {\tt ==} symbol, 68 |
10 \item {\tt ==} symbol, 69 |
11 \item {\tt ==>} symbol, 68 |
11 \item {\tt ==>} symbol, 69 |
12 \item {\tt =>} symbol, 68 |
12 \item {\tt =>} symbol, 69 |
13 \item {\tt =?=} symbol, 68 |
13 \item {\tt =?=} symbol, 69 |
14 \item {\tt\at Enum} constant, 91 |
14 \item {\tt\at Enum} constant, 92 |
15 \item {\tt\at Finset} constant, 91, 92 |
15 \item {\tt\at Finset} constant, 92, 93 |
16 \item {\tt [} symbol, 68 |
16 \item {\tt [} symbol, 69 |
17 \item {\tt [|} symbol, 68 |
17 \item {\tt [|} symbol, 69 |
18 \item {\tt ]} symbol, 68 |
18 \item {\tt ]} symbol, 69 |
19 \item {\tt _K} constant, 93, 95 |
19 \item {\tt _K} constant, 94, 96 |
20 \item \verb'{}' symbol, 91 |
20 \item \verb'{}' symbol, 92 |
21 \item {\tt\ttlbrace} symbol, 68 |
21 \item {\tt\ttlbrace} symbol, 69 |
22 \item {\tt\ttrbrace} symbol, 68 |
22 \item {\tt\ttrbrace} symbol, 69 |
23 \item {\tt |]} symbol, 68 |
23 \item {\tt |]} symbol, 69 |
24 |
24 |
25 \indexspace |
25 \indexspace |
26 |
26 |
27 \item {\tt Abs}, \bold{60}, 85 |
27 \item {\tt Abs}, \bold{60}, 86 |
28 \item {\tt abstract_over}, \bold{61} |
28 \item {\tt abstract_over}, \bold{61} |
29 \item {\tt abstract_rule}, \bold{45} |
29 \item {\tt abstract_rule}, \bold{45} |
30 \item {\tt aconv}, \bold{61} |
30 \item {\tt aconv}, \bold{61} |
31 \item {\tt addaltern}, \bold{132} |
31 \item {\tt addaltern}, \bold{133} |
32 \item {\tt addbefore}, \bold{132} |
32 \item {\tt addbefore}, \bold{133} |
33 \item {\tt Addcongs}, \bold{104} |
33 \item {\tt Addcongs}, \bold{105} |
34 \item {\tt addcongs}, \bold{108}, 123, 124 |
34 \item {\tt addcongs}, \bold{109}, 124, 125 |
35 \item {\tt AddDs}, \bold{136} |
35 \item {\tt AddDs}, \bold{137} |
36 \item {\tt addDs}, \bold{131} |
36 \item {\tt addDs}, \bold{132} |
37 \item {\tt addeqcongs}, \bold{108}, 123 |
37 \item {\tt addeqcongs}, \bold{109}, 124 |
38 \item {\tt AddEs}, \bold{136} |
38 \item {\tt AddEs}, \bold{137} |
39 \item {\tt addEs}, \bold{131} |
39 \item {\tt addEs}, \bold{132} |
40 \item {\tt AddIs}, \bold{136} |
40 \item {\tt AddIs}, \bold{137} |
41 \item {\tt addIs}, \bold{131} |
41 \item {\tt addIs}, \bold{132} |
42 \item {\tt addloop}, \bold{111} |
42 \item {\tt addloop}, \bold{112} |
43 \item {\tt addSaltern}, \bold{132} |
43 \item {\tt addSaltern}, \bold{133} |
44 \item {\tt addSbefore}, \bold{132} |
44 \item {\tt addSbefore}, \bold{133} |
45 \item {\tt AddSDs}, \bold{136} |
45 \item {\tt AddSDs}, \bold{137} |
46 \item {\tt addSDs}, \bold{131} |
46 \item {\tt addSDs}, \bold{132} |
47 \item {\tt AddSEs}, \bold{136} |
47 \item {\tt AddSEs}, \bold{137} |
48 \item {\tt addSEs}, \bold{131} |
48 \item {\tt addSEs}, \bold{132} |
49 \item {\tt Addsimprocs}, \bold{104} |
49 \item {\tt Addsimprocs}, \bold{105} |
50 \item {\tt addsimprocs}, \bold{107} |
50 \item {\tt addsimprocs}, \bold{108} |
51 \item {\tt Addsimps}, \bold{104} |
51 \item {\tt Addsimps}, \bold{105} |
52 \item {\tt addsimps}, \bold{106}, 124 |
52 \item {\tt addsimps}, \bold{107}, 125 |
53 \item {\tt AddSIs}, \bold{136} |
53 \item {\tt AddSIs}, \bold{137} |
54 \item {\tt addSIs}, \bold{131} |
54 \item {\tt addSIs}, \bold{132} |
55 \item {\tt addSolver}, \bold{110} |
55 \item {\tt addSolver}, \bold{111} |
56 \item {\tt addsplits}, \bold{111}, 124, 125 |
56 \item {\tt addsplits}, \bold{112}, 125, 126 |
57 \item {\tt addss}, \bold{132}, 133 |
57 \item {\tt addss}, \bold{133}, 134 |
58 \item {\tt addSSolver}, \bold{110} |
58 \item {\tt addSSolver}, \bold{111} |
59 \item {\tt all_tac}, \bold{31} |
59 \item {\tt all_tac}, \bold{31} |
60 \item {\tt ALLGOALS}, \bold{35}, 115, 118 |
60 \item {\tt ALLGOALS}, \bold{35}, 116, 119 |
61 \item ambiguity |
61 \item ambiguity |
62 \subitem of parsed expressions, 78 |
62 \subitem of parsed expressions, 79 |
63 \item {\tt ancestors_of}, \bold{59} |
63 \item {\tt ancestors_of}, \bold{59} |
64 \item {\tt any} nonterminal, \bold{67} |
64 \item {\tt any} nonterminal, \bold{68} |
65 \item {\tt APPEND}, \bold{29}, 31 |
65 \item {\tt APPEND}, \bold{29}, 31 |
66 \item {\tt APPEND'}, 36 |
66 \item {\tt APPEND'}, 36 |
67 \item {\tt Appl}, 82 |
67 \item {\tt Appl}, 83 |
68 \item {\tt aprop} nonterminal, \bold{69} |
68 \item {\tt aprop} nonterminal, \bold{70} |
69 \item {\tt ares_tac}, \bold{20} |
69 \item {\tt ares_tac}, \bold{20} |
70 \item {\tt args} nonterminal, 92 |
70 \item {\tt args} nonterminal, 93 |
71 \item {\tt Arith} theory, 117 |
71 \item {\tt Arith} theory, 118 |
72 \item arities |
72 \item arities |
73 \subitem context conditions, 54 |
73 \subitem context conditions, 54 |
74 \item {\tt Asm_full_simp_tac}, \bold{103} |
74 \item {\tt Asm_full_simp_tac}, \bold{104} |
75 \item {\tt asm_full_simp_tac}, 23, \bold{111}, 116 |
75 \item {\tt asm_full_simp_tac}, 23, \bold{112}, 117 |
76 \item {\tt asm_full_simplify}, 112 |
76 \item {\tt asm_full_simplify}, 113 |
77 \item {\tt asm_rl} theorem, 22 |
77 \item {\tt asm_rl} theorem, 22 |
78 \item {\tt Asm_simp_tac}, \bold{102}, 113 |
78 \item {\tt Asm_simp_tac}, \bold{103}, 114 |
79 \item {\tt asm_simp_tac}, \bold{111}, 124 |
79 \item {\tt asm_simp_tac}, \bold{112}, 125 |
80 \item {\tt asm_simplify}, 112 |
80 \item {\tt asm_simplify}, 113 |
81 \item associative-commutative operators, 117 |
81 \item associative-commutative operators, 118 |
82 \item {\tt assume}, \bold{43} |
82 \item {\tt assume}, \bold{43} |
83 \item {\tt assume_ax}, 9, \bold{57} |
83 \item {\tt assume_ax}, 9, \bold{57} |
84 \item {\tt assume_tac}, \bold{18}, 130 |
84 \item {\tt assume_tac}, \bold{18}, 131 |
85 \item {\tt assumption}, \bold{47} |
85 \item {\tt assumption}, \bold{47} |
86 \item assumptions |
86 \item assumptions |
87 \subitem contradictory, 137 |
87 \subitem contradictory, 138 |
88 \subitem deleting, 23 |
88 \subitem deleting, 23 |
89 \subitem in simplification, 102, 110 |
89 \subitem in simplification, 103, 111 |
90 \subitem inserting, 20 |
90 \subitem inserting, 20 |
91 \subitem negated, 128 |
91 \subitem negated, 129 |
92 \subitem of main goal, 8--10, 15 |
92 \subitem of main goal, 8--10, 15 |
93 \subitem reordering, 116 |
93 \subitem reordering, 117 |
94 \subitem rotating, 23 |
94 \subitem rotating, 23 |
95 \subitem substitution in, 99 |
95 \subitem substitution in, 100 |
96 \subitem tactics for, 18 |
96 \subitem tactics for, 18 |
97 \item ASTs, 82--87 |
97 \item ASTs, 83--88 |
98 \subitem made from parse trees, 83 |
98 \subitem made from parse trees, 84 |
99 \subitem made from terms, 85 |
99 \subitem made from terms, 86 |
100 \item {\tt atac}, \bold{20} |
100 \item {\tt atac}, \bold{20} |
101 \item {\tt Auto_tac}, \bold{136} |
101 \item {\tt Auto_tac}, \bold{137} |
102 \item {\tt axclass} section, 53 |
102 \item {\tt axclass} section, 53 |
103 \item axiomatic type class, 53 |
103 \item axiomatic type class, 53 |
104 \item axioms |
104 \item axioms |
105 \subitem extracting, 57 |
105 \subitem extracting, 57 |
106 \item {\tt axioms_of}, \bold{57} |
106 \item {\tt axioms_of}, \bold{57} |
113 \item {\tt bd}, \bold{12} |
113 \item {\tt bd}, \bold{12} |
114 \item {\tt bds}, \bold{12} |
114 \item {\tt bds}, \bold{12} |
115 \item {\tt be}, \bold{12} |
115 \item {\tt be}, \bold{12} |
116 \item {\tt bes}, \bold{12} |
116 \item {\tt bes}, \bold{12} |
117 \item {\tt BEST_FIRST}, \bold{32}, 33 |
117 \item {\tt BEST_FIRST}, \bold{32}, 33 |
118 \item {\tt Best_tac}, \bold{136} |
118 \item {\tt Best_tac}, \bold{137} |
119 \item {\tt best_tac}, \bold{135} |
119 \item {\tt best_tac}, \bold{136} |
120 \item {\tt beta_conversion}, \bold{45} |
120 \item {\tt beta_conversion}, \bold{45} |
121 \item {\tt bicompose}, \bold{47} |
121 \item {\tt bicompose}, \bold{47} |
122 \item {\tt bimatch_tac}, \bold{24} |
122 \item {\tt bimatch_tac}, \bold{24} |
123 \item {\tt bind_thm}, \bold{9}, 10, 38 |
123 \item {\tt bind_thm}, \bold{9}, 10, 38 |
124 \item binders, \bold{77} |
124 \item binders, \bold{78} |
125 \item {\tt biresolution}, \bold{47} |
125 \item {\tt biresolution}, \bold{47} |
126 \item {\tt biresolve_tac}, \bold{24}, 137 |
126 \item {\tt biresolve_tac}, \bold{24}, 138 |
127 \item {\tt Blast.depth_tac}, \bold{134} |
127 \item {\tt Blast.depth_tac}, \bold{135} |
128 \item {\tt Blast.trace}, \bold{134} |
128 \item {\tt Blast.trace}, \bold{135} |
129 \item {\tt Blast_tac}, \bold{136} |
129 \item {\tt Blast_tac}, \bold{137} |
130 \item {\tt blast_tac}, \bold{134} |
130 \item {\tt blast_tac}, \bold{135} |
131 \item {\tt Bound}, \bold{60}, 83, 85, 86 |
131 \item {\tt Bound}, \bold{60}, 84, 86, 87 |
132 \item {\tt bound_hyp_subst_tac}, \bold{99} |
132 \item {\tt bound_hyp_subst_tac}, \bold{100} |
133 \item {\tt br}, \bold{12} |
133 \item {\tt br}, \bold{12} |
134 \item {\tt BREADTH_FIRST}, \bold{32} |
134 \item {\tt BREADTH_FIRST}, \bold{32} |
135 \item {\tt brs}, \bold{12} |
135 \item {\tt brs}, \bold{12} |
136 \item {\tt bw}, \bold{13} |
136 \item {\tt bw}, \bold{13} |
137 \item {\tt bws}, \bold{13} |
137 \item {\tt bws}, \bold{13} |
138 \item {\tt by}, \bold{8}, 10, 11, 16 |
138 \item {\tt by}, \bold{8}, 10, 11, 16 |
139 \item {\tt byev}, \bold{8} |
139 \item {\tt byev}, \bold{8} |
140 |
140 |
141 \indexspace |
141 \indexspace |
142 |
142 |
143 \item {\tt cd}, \bold{3}, 55 |
143 \item {\tt cd}, \bold{3} |
144 \item {\tt cert_axm}, \bold{62} |
144 \item {\tt cert_axm}, \bold{62} |
145 \item {\tt CHANGED}, \bold{31} |
145 \item {\tt CHANGED}, \bold{31} |
146 \item {\tt chop}, \bold{10}, 14 |
146 \item {\tt chop}, \bold{10}, 14 |
147 \item {\tt choplev}, \bold{10} |
147 \item {\tt choplev}, \bold{10} |
148 \item {\tt Clarify_step_tac}, \bold{136} |
148 \item {\tt Clarify_step_tac}, \bold{137} |
149 \item {\tt clarify_step_tac}, \bold{133} |
149 \item {\tt clarify_step_tac}, \bold{134} |
150 \item {\tt Clarify_tac}, \bold{136} |
150 \item {\tt Clarify_tac}, \bold{137} |
151 \item {\tt clarify_tac}, \bold{133} |
151 \item {\tt clarify_tac}, \bold{134} |
152 \item claset |
152 \item claset |
153 \subitem current, 136 |
153 \subitem current, 137 |
154 \item {\tt claset} ML type, 130 |
154 \item {\tt claset} ML type, 131 |
155 \item classes |
155 \item classes |
156 \subitem context conditions, 54 |
156 \subitem context conditions, 54 |
157 \item classical reasoner, 126--138 |
157 \item classical reasoner, 127--139 |
158 \subitem setting up, 137 |
158 \subitem setting up, 138 |
159 \subitem tactics, 133 |
159 \subitem tactics, 134 |
160 \item classical sets, 130 |
160 \item classical sets, 131 |
161 \item {\tt ClassicalFun}, 138 |
161 \item {\tt ClassicalFun}, 139 |
162 \item {\tt combination}, \bold{45} |
162 \item {\tt combination}, \bold{45} |
163 \item {\tt commit}, \bold{2} |
163 \item {\tt commit}, \bold{2} |
164 \item {\tt COMP}, \bold{47} |
164 \item {\tt COMP}, \bold{47} |
165 \item {\tt compose}, \bold{47} |
165 \item {\tt compose}, \bold{47} |
166 \item {\tt compose_tac}, \bold{24} |
166 \item {\tt compose_tac}, \bold{24} |
167 \item {\tt compSWrapper}, \bold{132} |
167 \item {\tt compSWrapper}, \bold{133} |
168 \item {\tt compWrapper}, \bold{132} |
168 \item {\tt compWrapper}, \bold{133} |
169 \item {\tt concl_of}, \bold{40} |
169 \item {\tt concl_of}, \bold{40} |
170 \item {\tt COND}, \bold{33} |
170 \item {\tt COND}, \bold{33} |
171 \item congruence rules, 107 |
171 \item congruence rules, 108 |
172 \item {\tt Const}, \bold{60}, 85, 95 |
172 \item {\tt Const}, \bold{60}, 86, 96 |
173 \item {\tt Constant}, 82, 95 |
173 \item {\tt Constant}, 83, 96 |
174 \item constants, \bold{60} |
174 \item constants, \bold{60} |
175 \subitem for translations, 72 |
175 \subitem for translations, 73 |
176 \subitem syntactic, 87 |
176 \subitem syntactic, 88 |
177 \item {\tt context}, 102 |
177 \item {\tt context}, 103 |
178 \item {\tt contr_tac}, \bold{137} |
178 \item {\tt contr_tac}, \bold{138} |
179 \item {\tt could_unify}, \bold{26} |
179 \item {\tt could_unify}, \bold{26} |
180 \item {\tt cprems_of}, \bold{40} |
180 \item {\tt cprems_of}, \bold{40} |
181 \item {\tt cprop_of}, \bold{40} |
181 \item {\tt cprop_of}, \bold{40} |
182 \item {\tt CPure} theory, 51 |
182 \item {\tt CPure} theory, 51 |
183 \item {\tt CPure.thy}, \bold{58} |
183 \item {\tt CPure.thy}, \bold{58} |
185 \item {\tt cterm} ML type, 62 |
185 \item {\tt cterm} ML type, 62 |
186 \item {\tt cterm_instantiate}, \bold{39} |
186 \item {\tt cterm_instantiate}, \bold{39} |
187 \item {\tt cterm_of}, 8, 14, \bold{62} |
187 \item {\tt cterm_of}, 8, 14, \bold{62} |
188 \item {\tt ctyp}, \bold{63} |
188 \item {\tt ctyp}, \bold{63} |
189 \item {\tt ctyp_of}, \bold{64} |
189 \item {\tt ctyp_of}, \bold{64} |
190 \item {\tt cut_facts_tac}, 8, \bold{20}, 100 |
190 \item {\tt cut_facts_tac}, 8, \bold{20}, 101 |
191 \item {\tt cut_inst_tac}, \bold{20} |
191 \item {\tt cut_inst_tac}, \bold{20} |
192 \item {\tt cut_rl} theorem, 22 |
192 \item {\tt cut_rl} theorem, 22 |
193 |
193 |
194 \indexspace |
194 \indexspace |
195 |
195 |
196 \item {\tt datatype}, 104 |
196 \item {\tt datatype}, 105 |
197 \item {\tt Deepen_tac}, \bold{136} |
197 \item {\tt Deepen_tac}, \bold{137} |
198 \item {\tt deepen_tac}, \bold{135} |
198 \item {\tt deepen_tac}, \bold{136} |
199 \item {\tt defer_tac}, \bold{21} |
199 \item {\tt defer_tac}, \bold{21} |
200 \item definitions, \see{rewriting, meta-level}{1}, 21, \bold{53} |
200 \item definitions, \see{rewriting, meta-level}{1}, 21, \bold{54} |
201 \subitem unfolding, 8, 9 |
201 \subitem unfolding, 8, 9 |
202 \item {\tt Delcongs}, \bold{104} |
202 \item {\tt Delcongs}, \bold{105} |
203 \item {\tt delcongs}, \bold{108} |
203 \item {\tt delcongs}, \bold{109} |
204 \item {\tt deleqcongs}, \bold{108} |
204 \item {\tt deleqcongs}, \bold{109} |
205 \item {\tt delete_tmpfiles}, \bold{55} |
205 \item {\tt delete_tmpfiles}, \bold{55} |
206 \item delimiters, \bold{69}, 72, 73, 75 |
206 \item delimiters, \bold{70}, 73, 74, 76 |
207 \item {\tt delrules}, \bold{131} |
207 \item {\tt delrules}, \bold{132} |
208 \item {\tt Delsimprocs}, \bold{104} |
208 \item {\tt Delsimprocs}, \bold{105} |
209 \item {\tt delsimprocs}, \bold{107} |
209 \item {\tt delsimprocs}, \bold{108} |
210 \item {\tt Delsimps}, \bold{104} |
210 \item {\tt Delsimps}, \bold{105} |
211 \item {\tt delsimps}, \bold{106} |
211 \item {\tt delsimps}, \bold{107} |
212 \item {\tt dependent_tr'}, 93, \bold{95} |
212 \item {\tt dependent_tr'}, 94, \bold{96} |
213 \item {\tt DEPTH_FIRST}, \bold{32} |
213 \item {\tt DEPTH_FIRST}, \bold{32} |
214 \item {\tt DEPTH_SOLVE}, \bold{32} |
214 \item {\tt DEPTH_SOLVE}, \bold{32} |
215 \item {\tt DEPTH_SOLVE_1}, \bold{32} |
215 \item {\tt DEPTH_SOLVE_1}, \bold{32} |
216 \item {\tt depth_tac}, \bold{135} |
216 \item {\tt depth_tac}, \bold{136} |
217 \item {\tt Deriv.drop}, \bold{49} |
217 \item {\tt Deriv.drop}, \bold{49} |
218 \item {\tt Deriv.linear}, \bold{49} |
218 \item {\tt Deriv.linear}, \bold{49} |
219 \item {\tt Deriv.size}, \bold{49} |
219 \item {\tt Deriv.size}, \bold{49} |
220 \item {\tt Deriv.tree}, \bold{49} |
220 \item {\tt Deriv.tree}, \bold{49} |
221 \item {\tt dest_eq}, \bold{100} |
221 \item {\tt dest_eq}, \bold{101} |
222 \item {\tt dest_state}, \bold{41} |
222 \item {\tt dest_state}, \bold{41} |
223 \item destruct-resolution, 18 |
223 \item destruct-resolution, 18 |
224 \item {\tt DETERM}, \bold{33} |
224 \item {\tt DETERM}, \bold{33} |
225 \item discrimination nets, \bold{25} |
225 \item discrimination nets, \bold{25} |
226 \item {\tt distinct_subgoals_tac}, \bold{23} |
226 \item {\tt distinct_subgoals_tac}, \bold{23} |
227 \item {\tt dmatch_tac}, \bold{18} |
227 \item {\tt dmatch_tac}, \bold{18} |
228 \item {\tt dres_inst_tac}, \bold{19} |
228 \item {\tt dres_inst_tac}, \bold{19} |
229 \item {\tt dresolve_tac}, \bold{18} |
229 \item {\tt dresolve_tac}, \bold{18} |
230 \item {\tt dtac}, \bold{20} |
230 \item {\tt dtac}, \bold{20} |
231 \item {\tt dummyT}, 85, 86, 96 |
231 \item {\tt dummyT}, 86, 87, 97 |
232 \item duplicate subgoals |
232 \item duplicate subgoals |
233 \subitem removing, 23 |
233 \subitem removing, 23 |
234 |
234 |
235 \indexspace |
235 \indexspace |
236 |
236 |
237 \item elim-resolution, 17 |
237 \item elim-resolution, 17 |
238 \item {\tt ematch_tac}, \bold{18} |
238 \item {\tt ematch_tac}, \bold{18} |
239 \item {\tt empty} constant, 91 |
239 \item {\tt empty} constant, 92 |
240 \item {\tt empty_cs}, \bold{130} |
240 \item {\tt empty_cs}, \bold{131} |
241 \item {\tt empty_ss}, \bold{105} |
241 \item {\tt empty_ss}, \bold{106} |
242 \item {\tt eq_assume_tac}, \bold{18}, 130 |
242 \item {\tt eq_assume_tac}, \bold{18}, 131 |
243 \item {\tt eq_assumption}, \bold{47} |
243 \item {\tt eq_assumption}, \bold{47} |
244 \item {\tt eq_mp_tac}, \bold{137} |
244 \item {\tt eq_mp_tac}, \bold{138} |
245 \item {\tt eq_reflection} theorem, \bold{100}, 121 |
245 \item {\tt eq_reflection} theorem, \bold{101}, 122 |
246 \item {\tt eq_thm}, \bold{33} |
246 \item {\tt eq_thm}, \bold{33} |
247 \item {\tt eq_thy}, \bold{58} |
247 \item {\tt eq_thy}, \bold{58} |
248 \item {\tt equal_elim}, \bold{44} |
248 \item {\tt equal_elim}, \bold{44} |
249 \item {\tt equal_intr}, \bold{44} |
249 \item {\tt equal_intr}, \bold{44} |
250 \item equality, 98--101 |
250 \item equality, 99--102 |
251 \item {\tt eres_inst_tac}, \bold{19} |
251 \item {\tt eres_inst_tac}, \bold{19} |
252 \item {\tt eresolve_tac}, \bold{17} |
252 \item {\tt eresolve_tac}, \bold{17} |
253 \item {\tt ERROR}, 5 |
253 \item {\tt ERROR}, 5 |
254 \item {\tt error}, 5 |
254 \item {\tt error}, 5 |
255 \item error messages, 5 |
255 \item error messages, 5 |
256 \item {\tt eta_contract}, \bold{5}, 89 |
256 \item {\tt eta_contract}, \bold{5}, 90 |
257 \item {\tt etac}, \bold{20} |
257 \item {\tt etac}, \bold{20} |
258 \item {\tt EVERY}, \bold{30} |
258 \item {\tt EVERY}, \bold{30} |
259 \item {\tt EVERY'}, 36 |
259 \item {\tt EVERY'}, 36 |
260 \item {\tt EVERY1}, \bold{36} |
260 \item {\tt EVERY1}, \bold{36} |
261 \item examples |
261 \item examples |
262 \subitem of logic definitions, 79 |
262 \subitem of logic definitions, 80 |
263 \subitem of macros, 91, 92 |
263 \subitem of macros, 92, 93 |
264 \subitem of mixfix declarations, 74 |
264 \subitem of mixfix declarations, 75 |
265 \subitem of simplification, 112 |
265 \subitem of simplification, 113 |
266 \subitem of translations, 95 |
266 \subitem of translations, 96 |
267 \item exceptions |
267 \item exceptions |
268 \subitem printing of, 5 |
268 \subitem printing of, 5 |
269 \item {\tt exit}, \bold{2} |
269 \item {\tt exit}, \bold{2} |
270 \item {\tt extensional}, \bold{45} |
270 \item {\tt extensional}, \bold{45} |
271 |
271 |
272 \indexspace |
272 \indexspace |
273 |
273 |
274 \item {\tt fa}, \bold{12} |
274 \item {\tt fa}, \bold{12} |
275 \item {\tt Fast_tac}, \bold{136} |
275 \item {\tt Fast_tac}, \bold{137} |
276 \item {\tt fast_tac}, \bold{135} |
276 \item {\tt fast_tac}, \bold{136} |
277 \item {\tt fd}, \bold{12} |
277 \item {\tt fd}, \bold{12} |
278 \item {\tt fds}, \bold{12} |
278 \item {\tt fds}, \bold{12} |
279 \item {\tt fe}, \bold{12} |
279 \item {\tt fe}, \bold{12} |
280 \item {\tt fes}, \bold{12} |
280 \item {\tt fes}, \bold{12} |
281 \item files |
281 \item files |
282 \subitem reading, 3, 54 |
282 \subitem reading, 3, 55 |
283 \item {\tt filt_resolve_tac}, \bold{26} |
283 \item {\tt filt_resolve_tac}, \bold{26} |
284 \item {\tt FILTER}, \bold{31} |
284 \item {\tt FILTER}, \bold{31} |
285 \item {\tt filter_goal}, \bold{16} |
285 \item {\tt filter_goal}, \bold{16} |
286 \item {\tt filter_thms}, \bold{26} |
286 \item {\tt filter_thms}, \bold{26} |
287 \item {\tt findE}, \bold{10} |
287 \item {\tt findE}, \bold{10} |
332 \item {\tt goalw_cterm}, \bold{8} |
332 \item {\tt goalw_cterm}, \bold{8} |
333 |
333 |
334 \indexspace |
334 \indexspace |
335 |
335 |
336 \item {\tt has_fewer_prems}, \bold{33} |
336 \item {\tt has_fewer_prems}, \bold{33} |
337 \item higher-order pattern, \bold{107} |
337 \item higher-order pattern, \bold{108} |
338 \item {\tt HOL_basic_ss}, \bold{105} |
338 \item {\tt HOL_basic_ss}, \bold{106} |
339 \item {\tt hyp_subst_tac}, \bold{99} |
339 \item {\tt hyp_subst_tac}, \bold{100} |
340 \item {\tt hyp_subst_tacs}, \bold{138} |
340 \item {\tt hyp_subst_tacs}, \bold{139} |
341 \item {\tt HypsubstFun}, 100, 138 |
341 \item {\tt HypsubstFun}, 101, 139 |
342 |
342 |
343 \indexspace |
343 \indexspace |
344 |
344 |
345 \item {\tt id} nonterminal, \bold{69}, 83, 90 |
345 \item {\tt id} nonterminal, \bold{70}, 84, 91 |
346 \item identifiers, 69 |
346 \item identifiers, 70 |
347 \item {\tt idt} nonterminal, 89 |
347 \item {\tt idt} nonterminal, 90 |
348 \item {\tt idts} nonterminal, \bold{69}, 77 |
348 \item {\tt idts} nonterminal, \bold{70}, 78 |
349 \item {\tt IF_UNSOLVED}, \bold{33} |
349 \item {\tt IF_UNSOLVED}, \bold{33} |
350 \item {\tt iff_reflection} theorem, 121 |
350 \item {\tt iff_reflection} theorem, 122 |
351 \item {\tt IFOL_ss}, \bold{124} |
351 \item {\tt IFOL_ss}, \bold{125} |
352 \item {\tt imp_intr} theorem, \bold{100} |
352 \item {\tt imp_intr} theorem, \bold{101} |
353 \item {\tt implies_elim}, \bold{44} |
353 \item {\tt implies_elim}, \bold{44} |
354 \item {\tt implies_elim_list}, \bold{44} |
354 \item {\tt implies_elim_list}, \bold{44} |
355 \item {\tt implies_intr}, \bold{44} |
355 \item {\tt implies_intr}, \bold{44} |
356 \item {\tt implies_intr_hyps}, \bold{44} |
356 \item {\tt implies_intr_hyps}, \bold{44} |
357 \item {\tt implies_intr_list}, \bold{44} |
357 \item {\tt implies_intr_list}, \bold{44} |
358 \item {\tt incr_boundvars}, \bold{61}, 95 |
358 \item {\tt incr_boundvars}, \bold{61}, 96 |
359 \item {\tt indexname} ML type, 60, 70 |
359 \item {\tt indexname} ML type, 60, 71 |
360 \item infixes, \bold{76} |
360 \item infixes, \bold{77} |
361 \item {\tt insert} constant, 91 |
361 \item {\tt insert} constant, 92 |
362 \item {\tt inst_step_tac}, \bold{136} |
362 \item {\tt inst_step_tac}, \bold{137} |
363 \item {\tt instance} section, 53 |
363 \item {\tt instance} section, 53 |
364 \item {\tt instantiate}, \bold{46} |
364 \item {\tt instantiate}, \bold{46} |
365 \item {\tt instantiate'}, \bold{39}, 46 |
365 \item {\tt instantiate'}, \bold{39}, 46 |
366 \item instantiation, 18, 39, 46 |
366 \item instantiation, 18, 39, 46 |
367 \item {\tt INTLEAVE}, \bold{29}, 31 |
367 \item {\tt INTLEAVE}, \bold{29}, 31 |
368 \item {\tt INTLEAVE'}, 36 |
368 \item {\tt INTLEAVE'}, 36 |
369 \item {\tt invoke_oracle}, \bold{64} |
369 \item {\tt invoke_oracle}, \bold{64} |
370 \item {\tt is} nonterminal, 91 |
370 \item {\tt is} nonterminal, 92 |
371 |
371 |
372 \indexspace |
372 \indexspace |
373 |
373 |
374 \item {\tt joinrules}, \bold{137} |
374 \item {\tt joinrules}, \bold{138} |
375 |
375 |
376 \indexspace |
376 \indexspace |
377 |
377 |
378 \item {\tt keep_derivs}, \bold{49} |
378 \item {\tt keep_derivs}, \bold{49} |
379 |
379 |
380 \indexspace |
380 \indexspace |
381 |
381 |
382 \item $\lambda$-abstractions, 25, \bold{60} |
382 \item $\lambda$-abstractions, 25, \bold{60} |
383 \item $\lambda$-calculus, 43, 45, 69 |
383 \item $\lambda$-calculus, 43, 45, 70 |
384 \item {\tt lessb}, \bold{25} |
384 \item {\tt lessb}, \bold{25} |
385 \item lexer, \bold{69} |
385 \item lexer, \bold{70} |
386 \item {\tt lift_rule}, \bold{48} |
386 \item {\tt lift_rule}, \bold{48} |
387 \item lifting, 48 |
387 \item lifting, 48 |
388 \item {\tt loadpath}, \bold{55} |
388 \item {\tt loadpath}, \bold{55} |
389 \item {\tt logic} class, 69, 74 |
389 \item {\tt logic} class, 70, 75 |
390 \item {\tt logic} nonterminal, \bold{69} |
390 \item {\tt logic} nonterminal, \bold{70} |
391 \item {\tt Logic.auto_rename}, \bold{23} |
391 \item {\tt Logic.auto_rename}, \bold{23} |
392 \item {\tt Logic.set_rename_prefix}, \bold{22} |
392 \item {\tt Logic.set_rename_prefix}, \bold{22} |
393 \item {\tt loose_bnos}, \bold{61}, 96 |
393 \item {\tt long_names}, \bold{4} |
394 |
394 \item {\tt loose_bnos}, \bold{61}, 97 |
395 \indexspace |
395 |
396 |
396 \indexspace |
397 \item macros, 87--93 |
397 |
398 \item {\tt make_elim}, \bold{40}, 131 |
398 \item macros, 88--94 |
399 \item {\tt Match} exception, 95, 100 |
399 \item {\tt make_elim}, \bold{40}, 132 |
400 \item {\tt match_tac}, \bold{18}, 130 |
400 \item {\tt Match} exception, 96, 101 |
401 \item {\tt max_pri}, 67, \bold{73} |
401 \item {\tt match_tac}, \bold{18}, 131 |
402 \item {\tt merge_ss}, \bold{105} |
402 \item {\tt max_pri}, 68, \bold{74} |
|
403 \item {\tt merge_ss}, \bold{106} |
403 \item {\tt merge_theories}, \bold{58} |
404 \item {\tt merge_theories}, \bold{58} |
404 \item meta-assumptions, 34, 42, 43, 47 |
405 \item meta-assumptions, 34, 42, 43, 47 |
405 \subitem printing of, 4 |
406 \subitem printing of, 4 |
406 \item meta-equality, 43, 44 |
407 \item meta-equality, 43, 44 |
407 \item meta-implication, 43, 44 |
408 \item meta-implication, 43, 44 |
408 \item meta-quantifiers, 43, 45 |
409 \item meta-quantifiers, 43, 45 |
409 \item meta-rewriting, 8, 13, 14, \bold{21}, |
410 \item meta-rewriting, 8, 13, 14, \bold{21}, |
410 \seealso{tactics, theorems}{139} |
411 \seealso{tactics, theorems}{140} |
411 \subitem in theorems, 39 |
412 \subitem in theorems, 39 |
412 \item meta-rules, \see{meta-rules}{1}, 42--48 |
413 \item meta-rules, \see{meta-rules}{1}, 42--48 |
413 \item {\tt METAHYPS}, 16, \bold{34} |
414 \item {\tt METAHYPS}, 16, \bold{34} |
414 \item mixfix declarations, 52, 72--77 |
415 \item mixfix declarations, 52, 73--78 |
415 \item {\tt mk_case_split_tac}, \bold{125} |
416 \item {\tt mk_case_split_tac}, \bold{126} |
416 \item {\tt mk_simproc}, \bold{119} |
417 \item {\tt mk_simproc}, \bold{120} |
417 \item {\tt ML} section, 53, 94, 96 |
418 \item {\tt ML} section, 53, 95, 97 |
418 \item model checkers, 78 |
419 \item model checkers, 79 |
419 \item {\tt mp} theorem, \bold{138} |
420 \item {\tt mp} theorem, \bold{139} |
420 \item {\tt mp_tac}, \bold{137} |
421 \item {\tt mp_tac}, \bold{138} |
421 \item {\tt MRL}, \bold{38} |
422 \item {\tt MRL}, \bold{38} |
422 \item {\tt MRS}, \bold{38} |
423 \item {\tt MRS}, \bold{38} |
423 |
424 |
424 \indexspace |
425 \indexspace |
425 |
426 |
426 \item name tokens, \bold{69} |
427 \item name tokens, \bold{70} |
427 \item {\tt nat_cancel}, \bold{120} |
428 \item {\tt nat_cancel}, \bold{121} |
428 \item {\tt net_bimatch_tac}, \bold{25} |
429 \item {\tt net_bimatch_tac}, \bold{25} |
429 \item {\tt net_biresolve_tac}, \bold{25} |
430 \item {\tt net_biresolve_tac}, \bold{25} |
430 \item {\tt net_match_tac}, \bold{25} |
431 \item {\tt net_match_tac}, \bold{25} |
431 \item {\tt net_resolve_tac}, \bold{25} |
432 \item {\tt net_resolve_tac}, \bold{25} |
432 \item {\tt no_tac}, \bold{31} |
433 \item {\tt no_tac}, \bold{31} |
433 \item {\tt None}, \bold{27} |
434 \item {\tt None}, \bold{27} |
434 \item {\tt not_elim} theorem, \bold{138} |
435 \item {\tt not_elim} theorem, \bold{139} |
435 \item {\tt nprems_of}, \bold{41} |
436 \item {\tt nprems_of}, \bold{41} |
436 \item numerals, 69 |
437 \item numerals, 70 |
437 |
438 |
438 \indexspace |
439 \indexspace |
439 |
440 |
440 \item {\textit {o}} type, 79 |
441 \item {\textit {o}} type, 80 |
441 \item {\tt object}, 64 |
442 \item {\tt object}, 64 |
442 \item {\tt op} symbol, 76 |
443 \item {\tt op} symbol, 77 |
443 \item {\tt option} ML type, 27 |
444 \item {\tt option} ML type, 27 |
444 \item oracles, 64--65 |
445 \item oracles, 64--66 |
445 \item {\tt ORELSE}, \bold{29}, 31, 35 |
446 \item {\tt ORELSE}, \bold{29}, 31, 35 |
446 \item {\tt ORELSE'}, 36 |
447 \item {\tt ORELSE'}, 36 |
447 |
448 |
448 \indexspace |
449 \indexspace |
449 |
450 |
450 \item parameters |
451 \item parameters |
451 \subitem removing unused, 23 |
452 \subitem removing unused, 23 |
452 \subitem renaming, 13, 22, 48 |
453 \subitem renaming, 13, 22, 48 |
453 \item {\tt parents_of}, \bold{59} |
454 \item {\tt parents_of}, \bold{59} |
454 \item parse trees, 82 |
455 \item parse trees, 83 |
455 \item {\tt parse_ast_translation}, 94 |
456 \item {\tt parse_ast_translation}, 95 |
456 \item {\tt parse_rules}, 89 |
457 \item {\tt parse_rules}, 90 |
457 \item {\tt parse_translation}, 94 |
458 \item {\tt parse_translation}, 95 |
458 \item pattern, higher-order, \bold{107} |
459 \item pattern, higher-order, \bold{108} |
459 \item {\tt pause_tac}, \bold{27} |
460 \item {\tt pause_tac}, \bold{27} |
460 \item Poly/{\ML} compiler, 5 |
461 \item Poly/{\ML} compiler, 5 |
461 \item {\tt pop_proof}, \bold{15} |
462 \item {\tt pop_proof}, \bold{15} |
462 \item {\tt pr}, \bold{11} |
463 \item {\tt pr}, \bold{11} |
463 \item {\tt premises}, \bold{8}, 15 |
464 \item {\tt premises}, \bold{8}, 15 |
464 \item {\tt prems_of}, \bold{40} |
465 \item {\tt prems_of}, \bold{40} |
465 \item {\tt prems_of_ss}, \bold{109} |
466 \item {\tt prems_of_ss}, \bold{110} |
466 \item pretty printing, 73, 75--76, 92 |
467 \item pretty printing, 74, 76--77, 93 |
467 \item {\tt Pretty.setdepth}, \bold{4} |
468 \item {\tt Pretty.setdepth}, \bold{4} |
468 \item {\tt Pretty.setmargin}, \bold{4} |
469 \item {\tt Pretty.setmargin}, \bold{4} |
469 \item {\tt PRIMITIVE}, \bold{26} |
470 \item {\tt PRIMITIVE}, \bold{26} |
470 \item {\tt primrec}, 104 |
471 \item {\tt primrec}, 105 |
471 \item {\tt prin}, 6, \bold{15} |
472 \item {\tt prin}, 6, \bold{15} |
472 \item print mode, 52, 96 |
473 \item print mode, 52, 97 |
473 \item print modes, 77--78 |
474 \item print modes, 78--79 |
474 \item {\tt print_ast_translation}, 94 |
475 \item {\tt print_ast_translation}, 95 |
475 \item {\tt print_cs}, \bold{130} |
476 \item {\tt print_cs}, \bold{131} |
476 \item {\tt print_data}, \bold{59} |
477 \item {\tt print_data}, \bold{59} |
477 \item {\tt print_depth}, \bold{4} |
478 \item {\tt print_depth}, \bold{4} |
478 \item {\tt print_exn}, \bold{6}, 37 |
479 \item {\tt print_exn}, \bold{6}, 37 |
479 \item {\tt print_goals}, \bold{38} |
480 \item {\tt print_goals}, \bold{38} |
480 \item {\tt print_mode}, 77 |
481 \item {\tt print_mode}, 78 |
481 \item {\tt print_modes}, 72 |
482 \item {\tt print_modes}, 73 |
482 \item {\tt print_rules}, 89 |
483 \item {\tt print_rules}, 90 |
483 \item {\tt print_simpset}, \bold{106} |
484 \item {\tt print_simpset}, \bold{107} |
484 \item {\tt print_ss}, \bold{105} |
485 \item {\tt print_ss}, \bold{106} |
485 \item {\tt print_syntax}, \bold{59}, \bold{71} |
486 \item {\tt print_syntax}, \bold{59}, \bold{72} |
486 \item {\tt print_tac}, \bold{27} |
487 \item {\tt print_tac}, \bold{27} |
487 \item {\tt print_theory}, \bold{59} |
488 \item {\tt print_theory}, \bold{59} |
488 \item {\tt print_thm}, \bold{38} |
489 \item {\tt print_thm}, \bold{38} |
489 \item {\tt print_translation}, 94 |
490 \item {\tt print_translation}, 95 |
490 \item printing control, 3--5 |
491 \item printing control, 3--5 |
491 \item {\tt printyp}, \bold{15} |
492 \item {\tt printyp}, \bold{15} |
492 \item priorities, 66, \bold{73} |
493 \item priorities, 67, \bold{74} |
493 \item priority grammars, 66--67 |
494 \item priority grammars, 67--68 |
494 \item {\tt prlev}, \bold{11} |
495 \item {\tt prlev}, \bold{11} |
495 \item {\tt prlim}, \bold{11} |
496 \item {\tt prlim}, \bold{11} |
496 \item productions, 66, 72, 73 |
497 \item productions, 67, 73, 74 |
497 \subitem copy, \bold{72}, 73, 84 |
498 \subitem copy, \bold{73}, 74, 85 |
498 \item {\tt proof} ML type, 15 |
499 \item {\tt proof} ML type, 15 |
499 \item proof objects, 48--50 |
500 \item proof objects, 48--50 |
500 \item proof state, 7 |
501 \item proof state, 7 |
501 \subitem printing of, 11 |
502 \subitem printing of, 11 |
502 \item {\tt proof_timing}, \bold{11} |
503 \item {\tt proof_timing}, \bold{11} |
588 \item rules |
589 \item rules |
589 \subitem converting destruction to elimination, 40 |
590 \subitem converting destruction to elimination, 40 |
590 |
591 |
591 \indexspace |
592 \indexspace |
592 |
593 |
593 \item {\tt safe_asm_full_simp_tac}, \bold{111} |
594 \item {\tt safe_asm_full_simp_tac}, \bold{112} |
594 \item {\tt Safe_step_tac}, \bold{136} |
595 \item {\tt Safe_step_tac}, \bold{137} |
595 \item {\tt safe_step_tac}, 131, \bold{135} |
596 \item {\tt safe_step_tac}, 132, \bold{136} |
596 \item {\tt Safe_tac}, \bold{136} |
597 \item {\tt Safe_tac}, \bold{137} |
597 \item {\tt safe_tac}, \bold{135} |
598 \item {\tt safe_tac}, \bold{136} |
598 \item {\tt save_proof}, \bold{15} |
599 \item {\tt save_proof}, \bold{15} |
599 \item saving your work, \bold{1} |
600 \item saving your work, \bold{1} |
600 \item search, 29 |
601 \item search, 29 |
601 \subitem tacticals, 31--33 |
602 \subitem tacticals, 31--33 |
602 \item {\tt SELECT_GOAL}, 21, \bold{34} |
603 \item {\tt SELECT_GOAL}, 21, \bold{34} |
603 \item {\tt Seq.seq} ML type, 26 |
604 \item {\tt Seq.seq} ML type, 26 |
604 \item sequences (lazy lists), \bold{27} |
605 \item sequences (lazy lists), \bold{27} |
605 \item sequent calculus, 127 |
606 \item sequent calculus, 128 |
606 \item sessions, 1--6 |
607 \item sessions, 1--6 |
607 \item {\tt set}, 3 |
608 \item {\tt set}, 3 |
608 \item {\tt setloop}, \bold{111} |
609 \item {\tt setloop}, \bold{112} |
609 \item {\tt setmksimps}, 106, \bold{122}, 124 |
610 \item {\tt setmksimps}, 107, \bold{123}, 125 |
610 \item {\tt setSolver}, \bold{110}, 124 |
611 \item {\tt setSolver}, \bold{111}, 125 |
611 \item {\tt setSSolver}, \bold{110}, 124 |
612 \item {\tt setSSolver}, \bold{111}, 125 |
612 \item {\tt setsubgoaler}, \bold{109}, 124 |
613 \item {\tt setsubgoaler}, \bold{110}, 125 |
613 \item {\tt setSWrapper}, \bold{132} |
614 \item {\tt setSWrapper}, \bold{133} |
614 \item {\tt settermless}, \bold{116} |
615 \item {\tt settermless}, \bold{117} |
615 \item {\tt setWrapper}, \bold{132} |
616 \item {\tt setWrapper}, \bold{133} |
616 \item shortcuts |
617 \item shortcuts |
617 \subitem for tactics, 19 |
618 \subitem for tactics, 19 |
618 \subitem for {\tt by} commands, 11 |
619 \subitem for {\tt by} commands, 11 |
619 \item {\tt show_brackets}, \bold{4} |
620 \item {\tt show_brackets}, \bold{4} |
620 \item {\tt show_consts}, \bold{4} |
621 \item {\tt show_consts}, \bold{4} |
621 \item {\tt show_hyps}, \bold{4} |
622 \item {\tt show_hyps}, \bold{4} |
622 \item {\tt show_sorts}, \bold{4}, 86, 94 |
623 \item {\tt show_sorts}, \bold{4}, 87, 95 |
623 \item {\tt show_types}, \bold{4}, 86, 89, 96 |
624 \item {\tt show_types}, \bold{4}, 87, 90, 97 |
|
625 \item {\tt Sign.certify_term}, \bold{62} |
|
626 \item {\tt Sign.certify_typ}, \bold{64} |
624 \item {\tt Sign.sg} ML type, 51 |
627 \item {\tt Sign.sg} ML type, 51 |
625 \item {\tt Sign.stamp_names_of}, \bold{59} |
628 \item {\tt Sign.stamp_names_of}, \bold{59} |
626 \item {\tt Sign.string_of_term}, \bold{62} |
629 \item {\tt Sign.string_of_term}, \bold{62} |
627 \item {\tt Sign.string_of_typ}, \bold{63} |
630 \item {\tt Sign.string_of_typ}, \bold{63} |
628 \item {\tt sign_of}, 8, 14, \bold{59} |
631 \item {\tt sign_of}, 8, 14, \bold{59} |
629 \item {\tt sign_of_thm}, \bold{41} |
632 \item {\tt sign_of_thm}, \bold{41} |
630 \item signatures, \bold{51}, 59, 61, 62, 64 |
633 \item signatures, \bold{51}, 59, 61, 62, 64 |
631 \item {\tt Simp_tac}, \bold{102} |
634 \item {\tt Simp_tac}, \bold{103} |
632 \item {\tt simp_tac}, \bold{111} |
635 \item {\tt simp_tac}, \bold{112} |
633 \item simplification, 102--125 |
636 \item simplification, 103--126 |
634 \subitem forward rules, 112 |
637 \subitem forward rules, 113 |
635 \subitem from classical reasoner, 132 |
638 \subitem from classical reasoner, 133 |
636 \subitem setting up, 121 |
639 \subitem setting up, 122 |
637 \subitem tactics, 111 |
640 \subitem tactics, 112 |
638 \item simplification sets, 105 |
641 \item simplification sets, 106 |
639 \item {\tt simplify}, 112 |
642 \item {\tt simplify}, 113 |
640 \item {\tt SIMPSET}, \bold{111} |
643 \item {\tt SIMPSET}, \bold{112} |
641 \item simpset |
644 \item simpset |
642 \subitem current, 102, 106 |
645 \subitem current, 103, 107 |
643 \item {\tt simpset}, \bold{106} |
646 \item {\tt simpset}, \bold{107} |
644 \item {\tt SIMPSET'}, \bold{111} |
647 \item {\tt SIMPSET'}, \bold{112} |
645 \item {\tt simpset_of}, \bold{106} |
648 \item {\tt simpset_of}, \bold{107} |
646 \item {\tt simpset_ref}, \bold{106} |
649 \item {\tt simpset_ref}, \bold{107} |
647 \item {\tt simpset_ref_of}, \bold{106} |
650 \item {\tt simpset_ref_of}, \bold{107} |
648 \item {\tt simpset_thy_data}, \bold{125} |
651 \item {\tt simpset_thy_data}, \bold{126} |
649 \item {\tt size_of_thm}, 32, \bold{33}, 138 |
652 \item {\tt size_of_thm}, 32, \bold{33}, 139 |
650 \item {\tt sizef}, \bold{138} |
653 \item {\tt sizef}, \bold{139} |
651 \item {\tt slow_best_tac}, \bold{135} |
654 \item {\tt slow_best_tac}, \bold{136} |
652 \item {\tt slow_step_tac}, 132, \bold{136} |
655 \item {\tt slow_step_tac}, 133, \bold{137} |
653 \item {\tt slow_tac}, \bold{135} |
656 \item {\tt slow_tac}, \bold{136} |
654 \item {\tt Some}, \bold{27} |
657 \item {\tt Some}, \bold{27} |
655 \item {\tt SOMEGOAL}, \bold{35} |
658 \item {\tt SOMEGOAL}, \bold{35} |
656 \item {\tt sort} nonterminal, \bold{69} |
659 \item {\tt sort} nonterminal, \bold{70} |
657 \item sort constraints, 68 |
660 \item sort constraints, 69 |
658 \item sort hypotheses, 41 |
661 \item sort hypotheses, 41 |
659 \item sorts |
662 \item sorts |
660 \subitem printing of, 4 |
663 \subitem printing of, 4 |
661 \item {\tt split_tac}, \bold{125} |
664 \item {\tt split_tac}, \bold{126} |
662 \item {\tt ssubst} theorem, \bold{98} |
665 \item {\tt ssubst} theorem, \bold{99} |
663 \item {\tt stac}, \bold{99} |
666 \item {\tt stac}, \bold{100} |
664 \item stamps, \bold{51}, 59 |
667 \item stamps, \bold{51}, 59 |
665 \item {\tt standard}, \bold{40} |
668 \item {\tt standard}, \bold{40} |
666 \item starting up, \bold{1} |
669 \item starting up, \bold{1} |
667 \item {\tt Step_tac}, \bold{136} |
670 \item {\tt Step_tac}, \bold{137} |
668 \item {\tt step_tac}, 132, \bold{136} |
671 \item {\tt step_tac}, 133, \bold{137} |
669 \item {\tt store_thm}, \bold{9} |
672 \item {\tt store_thm}, \bold{9} |
670 \item {\tt string_of_cterm}, \bold{62} |
673 \item {\tt string_of_cterm}, \bold{62} |
671 \item {\tt string_of_ctyp}, \bold{63} |
674 \item {\tt string_of_ctyp}, \bold{63} |
672 \item {\tt string_of_thm}, \bold{38} |
675 \item {\tt string_of_thm}, \bold{38} |
673 \item strings, 69 |
676 \item strings, 70 |
674 \item {\tt SUBGOAL}, \bold{26} |
677 \item {\tt SUBGOAL}, \bold{26} |
675 \item subgoal module, 7--16 |
678 \item subgoal module, 7--16 |
676 \item {\tt subgoal_tac}, \bold{20} |
679 \item {\tt subgoal_tac}, \bold{20} |
677 \item {\tt subgoals_of_brl}, \bold{24} |
680 \item {\tt subgoals_of_brl}, \bold{24} |
678 \item {\tt subgoals_tac}, \bold{20} |
681 \item {\tt subgoals_tac}, \bold{20} |
679 \item {\tt subst} theorem, 98, \bold{100} |
682 \item {\tt subst} theorem, 99, \bold{101} |
680 \item substitution |
683 \item substitution |
681 \subitem rules, 98 |
684 \subitem rules, 99 |
682 \item {\tt subthy}, \bold{58} |
685 \item {\tt subthy}, \bold{58} |
683 \item {\tt swap} theorem, \bold{138} |
686 \item {\tt swap} theorem, \bold{139} |
684 \item {\tt swap_res_tac}, \bold{137} |
687 \item {\tt swap_res_tac}, \bold{138} |
685 \item {\tt swapify}, \bold{137} |
688 \item {\tt swapify}, \bold{138} |
686 \item {\tt sym} theorem, 99, \bold{100} |
689 \item {\tt sym} theorem, 100, \bold{101} |
687 \item {\tt symmetric}, \bold{44} |
690 \item {\tt symmetric}, \bold{44} |
688 \item {\tt syn_of}, \bold{71} |
691 \item {\tt syn_of}, \bold{72} |
689 \item syntax |
692 \item syntax |
690 \subitem Pure, 67--72 |
693 \subitem Pure, 68--73 |
691 \subitem transformations, 82--96 |
694 \subitem transformations, 83--97 |
692 \item {\tt syntax} section, 52 |
695 \item {\tt syntax} section, 52 |
693 \item {\tt Syntax.ast} ML type, 82 |
696 \item {\tt Syntax.ast} ML type, 83 |
694 \item {\tt Syntax.mark_boundT}, 96 |
697 \item {\tt Syntax.mark_boundT}, 97 |
695 \item {\tt Syntax.print_gram}, \bold{71} |
698 \item {\tt Syntax.print_gram}, \bold{72} |
696 \item {\tt Syntax.print_syntax}, \bold{71} |
699 \item {\tt Syntax.print_syntax}, \bold{72} |
697 \item {\tt Syntax.print_trans}, \bold{71} |
700 \item {\tt Syntax.print_trans}, \bold{72} |
698 \item {\tt Syntax.stat_norm_ast}, 91 |
701 \item {\tt Syntax.stat_norm_ast}, 92 |
699 \item {\tt Syntax.syntax} ML type, 71 |
702 \item {\tt Syntax.syntax} ML type, 72 |
700 \item {\tt Syntax.test_read}, 75, 91 |
703 \item {\tt Syntax.test_read}, 76, 92 |
701 \item {\tt Syntax.trace_norm_ast}, 91 |
704 \item {\tt Syntax.trace_norm_ast}, 92 |
702 \item {\tt Syntax.variant_abs'}, 96 |
705 \item {\tt Syntax.variant_abs'}, 97 |
703 |
706 |
704 \indexspace |
707 \indexspace |
705 |
708 |
706 \item {\tt tactic} ML type, 17 |
709 \item {\tt tactic} ML type, 17 |
707 \item tacticals, 29--36 |
710 \item tacticals, 29--36 |
774 \item {\tt thin_tac}, \bold{23} |
777 \item {\tt thin_tac}, \bold{23} |
775 \item {\tt THM} exception, 37, 38, 42, 47 |
778 \item {\tt THM} exception, 37, 38, 42, 47 |
776 \item {\tt thm} ML type, 37 |
779 \item {\tt thm} ML type, 37 |
777 \item {\tt thms_containing}, \bold{10} |
780 \item {\tt thms_containing}, \bold{10} |
778 \item {\tt thms_of}, \bold{57} |
781 \item {\tt thms_of}, \bold{57} |
779 \item {\tt thy_data}, \bold{125} |
782 \item {\tt thy_data}, \bold{126} |
780 \item {\tt tid} nonterminal, \bold{69}, 83, 90 |
783 \item {\tt tid} nonterminal, \bold{70}, 84, 91 |
781 \item {\tt time_use}, \bold{3} |
784 \item {\tt time_use}, \bold{3} |
782 \item {\tt time_use_thy}, \bold{55} |
785 \item {\tt time_use_thy}, \bold{55} |
783 \item timing statistics, 11 |
786 \item timing statistics, 11 |
784 \item {\tt toggle}, 3 |
787 \item {\tt toggle}, 3 |
785 \item token class, 96 |
788 \item token class, 97 |
786 \item token translations, 96--97 |
789 \item token translations, 97--98 |
787 \item token_translation, 97 |
790 \item token_translation, 98 |
788 \item {\tt token_translation}, 97 |
791 \item {\tt token_translation}, 98 |
789 \item {\tt topthm}, \bold{16} |
792 \item {\tt topthm}, \bold{16} |
790 \item {\tt tpairs_of}, \bold{41} |
793 \item {\tt tpairs_of}, \bold{41} |
791 \item {\tt trace_BEST_FIRST}, \bold{32} |
794 \item {\tt trace_BEST_FIRST}, \bold{32} |
792 \item {\tt trace_DEPTH_FIRST}, \bold{32} |
795 \item {\tt trace_DEPTH_FIRST}, \bold{32} |
793 \item {\tt trace_goalno_tac}, \bold{35} |
796 \item {\tt trace_goalno_tac}, \bold{35} |
794 \item {\tt trace_REPEAT}, \bold{30} |
797 \item {\tt trace_REPEAT}, \bold{30} |
795 \item {\tt trace_simp}, \bold{103}, 114 |
798 \item {\tt trace_simp}, \bold{104}, 115 |
796 \item tracing |
799 \item tracing |
797 \subitem of classical prover, 134 |
800 \subitem of classical prover, 135 |
798 \subitem of macros, 91 |
801 \subitem of macros, 92 |
799 \subitem of searching tacticals, 32 |
802 \subitem of searching tacticals, 32 |
800 \subitem of simplification, 103, 114--115 |
803 \subitem of simplification, 104, 115--116 |
801 \subitem of tactics, 27 |
804 \subitem of tactics, 27 |
802 \subitem of unification, 42 |
805 \subitem of unification, 42 |
803 \item {\tt transfer}, \bold{58} |
806 \item {\tt transfer}, \bold{58} |
804 \item {\tt transfer_sg}, \bold{58} |
807 \item {\tt transfer_sg}, \bold{58} |
805 \item {\tt transitive}, \bold{45} |
808 \item {\tt transitive}, \bold{45} |
806 \item translations, 93--96 |
809 \item translations, 94--97 |
807 \subitem parse, 77, 85 |
810 \subitem parse, 78, 86 |
808 \subitem parse AST, \bold{83}, 84 |
811 \subitem parse AST, \bold{84}, 85 |
809 \subitem print, 77 |
812 \subitem print, 78 |
810 \subitem print AST, \bold{86} |
813 \subitem print AST, \bold{87} |
811 \item {\tt translations} section, 88 |
814 \item {\tt translations} section, 89 |
812 \item {\tt trivial}, \bold{48} |
815 \item {\tt trivial}, \bold{48} |
813 \item {\tt Trueprop} constant, 79 |
816 \item {\tt Trueprop} constant, 80 |
814 \item {\tt TRY}, \bold{30, 31} |
817 \item {\tt TRY}, \bold{30, 31} |
815 \item {\tt TRYALL}, \bold{35} |
818 \item {\tt TRYALL}, \bold{35} |
816 \item {\tt TVar}, \bold{63} |
819 \item {\tt TVar}, \bold{63} |
817 \item {\tt tvar} nonterminal, \bold{69, 70}, 83, 90 |
820 \item {\tt tvar} nonterminal, \bold{70, 71}, 84, 91 |
818 \item {\tt typ} ML type, 63 |
821 \item {\tt typ} ML type, 63 |
819 \item {\tt Type}, \bold{63} |
822 \item {\tt Type}, \bold{63} |
820 \item {\textit {type}} type, 74 |
823 \item {\textit {type}} type, 75 |
821 \item {\tt type} nonterminal, \bold{69} |
824 \item {\tt type} nonterminal, \bold{70} |
822 \item type constraints, 69, 77, 86 |
825 \item type constraints, 70, 78, 87 |
823 \item type constructors, \bold{63} |
826 \item type constructors, \bold{63} |
824 \item type identifiers, 69 |
827 \item type identifiers, 70 |
825 \item type synonyms, \bold{52} |
828 \item type synonyms, \bold{52} |
826 \item type unknowns, \bold{63}, 69 |
829 \item type unknowns, \bold{63}, 70 |
827 \subitem freezing/thawing of, 46 |
830 \subitem freezing/thawing of, 46 |
828 \item type variables, \bold{63} |
831 \item type variables, \bold{63} |
829 \item {\tt typed_print_translation}, 94 |
832 \item {\tt typed_print_translation}, 95 |
830 \item types, \bold{63} |
833 \item types, \bold{63} |
831 \subitem certified, \bold{63} |
834 \subitem certified, \bold{63} |
832 \subitem printing of, 4, 15, 63 |
835 \subitem printing of, 4, 15, 63 |
833 |
836 |
834 \indexspace |
837 \indexspace |
835 |
838 |
836 \item {\tt undo}, 7, \bold{10}, 14 |
839 \item {\tt undo}, 7, \bold{10}, 14 |
837 \item unknowns, \bold{60}, 69 |
840 \item unknowns, \bold{60}, 70 |
838 \item {\tt unlink_thy}, \bold{56} |
841 \item {\tt unlink_thy}, \bold{56} |
839 \item {\tt update}, \bold{56} |
842 \item {\tt update}, \bold{56} |
840 \item {\tt uresult}, \bold{9}, 16, 57 |
843 \item {\tt uresult}, \bold{9}, 16, 57 |
841 \item {\tt use}, \bold{3} |
844 \item {\tt use}, \bold{3} |
842 \item {\tt use_thy}, \bold{54}, 55 |
845 \item {\tt use_thy}, \bold{55} |
843 |
846 |
844 \indexspace |
847 \indexspace |
845 |
848 |
846 \item {\tt Var}, \bold{60}, 85 |
849 \item {\tt Var}, \bold{60}, 86 |
847 \item {\tt var} nonterminal, \bold{69, 70}, 83, 90 |
850 \item {\tt var} nonterminal, \bold{70, 71}, 84, 91 |
848 \item {\tt Variable}, 82 |
851 \item {\tt Variable}, 83 |
849 \item variables |
852 \item variables |
850 \subitem bound, \bold{60} |
853 \subitem bound, \bold{60} |
851 \subitem free, \bold{60} |
854 \subitem free, \bold{60} |
852 \item {\tt variant_abs}, \bold{61} |
855 \item {\tt variant_abs}, \bold{61} |
853 \item {\tt varifyT}, \bold{46} |
856 \item {\tt varifyT}, \bold{46} |