1 \begin{theindex} |
1 \begin{theindex} |
2 |
2 |
3 \item {\ptt !!} symbol, 64 |
3 \item {\tt !!} symbol, 65 |
4 \subitem in main goal, 7 |
4 \subitem in main goal, 7 |
5 \item {\tt\$}, \bold{56}, 79 |
5 \item {\tt\$}, \bold{57}, 82 |
6 \item {\tt\%} symbol, 64 |
6 \item {\tt\%} symbol, 65 |
7 \item * |
7 \item * |
8 \subitem claset, 121 |
8 \subitem claset, 127 |
9 \subitem simpset, 99 |
9 \subitem simpset, 106 |
10 \item {\ptt ::} symbol, 64, 65 |
10 \item {\tt ::} symbol, 65, 66 |
11 \item {\ptt ==} symbol, 64 |
11 \item {\tt ==} symbol, 65 |
12 \item {\ptt ==>} symbol, 64 |
12 \item {\tt ==>} symbol, 65 |
13 \item {\ptt =>} symbol, 64 |
13 \item {\tt =>} symbol, 65 |
14 \item {\ptt =?=} symbol, 64 |
14 \item {\tt =?=} symbol, 65 |
15 \item {\tt\at Enum} constant, 85 |
15 \item {\tt\at Enum} constant, 88 |
16 \item {\tt\at Finset} constant, 85 |
16 \item {\tt\at Finset} constant, 88, 89 |
17 \item {\ptt [} symbol, 64 |
17 \item {\tt [} symbol, 65 |
18 \item {\ptt [|} symbol, 64 |
18 \item {\tt [|} symbol, 65 |
19 \item {\ptt ]} symbol, 64 |
19 \item {\tt ]} symbol, 65 |
20 \item {\ptt _K} constant, 86, 88 |
20 \item {\tt _K} constant, 90, 92 |
21 \item \verb'{}' symbol, 85 |
21 \item \verb'{}' symbol, 88 |
22 \item {\tt\ttlbrace} symbol, 64 |
22 \item {\tt\ttlbrace} symbol, 65 |
23 \item {\tt\ttrbrace} symbol, 64 |
23 \item {\tt\ttrbrace} symbol, 65 |
24 \item {\ptt |]} symbol, 64 |
24 \item {\tt |]} symbol, 65 |
25 |
25 |
26 \indexspace |
26 \indexspace |
27 |
27 |
28 \item {\ptt Abs}, \bold{56}, 79 |
28 \item {\tt Abs}, \bold{57}, 82 |
29 \item {\ptt abstract_over}, \bold{57} |
29 \item {\tt abstract_over}, \bold{58} |
30 \item {\ptt abstract_rule}, \bold{41} |
30 \item {\tt abstract_rule}, \bold{44} |
31 \item {\ptt aconv}, \bold{57} |
31 \item {\tt aconv}, \bold{58} |
32 \item {\ptt addaltern}, \bold{118} |
32 \item {\tt addaltern}, \bold{124} |
33 \item {\ptt addbefore}, \bold{118} |
33 \item {\tt addbefore}, \bold{124} |
34 \item {\ptt addcongs}, 97, 110, \bold{110} |
34 \item {\tt addcongs}, 103, \bold{115}, 116 |
35 \item {\ptt AddDs}, \bold{121} |
35 \item {\tt AddDs}, \bold{127} |
36 \item {\ptt addDs}, \bold{116} |
36 \item {\tt addDs}, \bold{123} |
37 \item {\ptt addeqcongs}, \bold{97}, 100, 110 |
37 \item {\tt addeqcongs}, \bold{103}, 105, 115 |
38 \item {\ptt AddEs}, \bold{121} |
38 \item {\tt AddEs}, \bold{127} |
39 \item {\ptt addEs}, \bold{116} |
39 \item {\tt addEs}, \bold{123} |
40 \item {\ptt AddIs}, \bold{121} |
40 \item {\tt AddIs}, \bold{127} |
41 \item {\ptt addIs}, \bold{116} |
41 \item {\tt addIs}, \bold{123} |
42 \item {\ptt addloop}, 99, 100 |
42 \item {\tt addloop}, 104, 105 |
43 \item {\ptt addSaltern}, \bold{118} |
43 \item {\tt addSaltern}, \bold{124} |
44 \item {\ptt addSbefore}, \bold{118} |
44 \item {\tt addSbefore}, \bold{124} |
45 \item {\ptt AddSDs}, \bold{121} |
45 \item {\tt AddSDs}, \bold{127} |
46 \item {\ptt addSDs}, \bold{116} |
46 \item {\tt addSDs}, \bold{123} |
47 \item {\ptt AddSEs}, \bold{121} |
47 \item {\tt AddSEs}, \bold{127} |
48 \item {\ptt addSEs}, \bold{116} |
48 \item {\tt addSEs}, \bold{123} |
49 \item {\ptt Addsimps}, \bold{95}, 99, 100 |
49 \item {\tt Addsimps}, \bold{100}, 105, 106 |
50 \item {\ptt addsimps}, 96, 99, 100, 110 |
50 \item {\tt addsimps}, 102, 105, 106, 116 |
51 \item {\ptt AddSIs}, \bold{121} |
51 \item {\tt AddSIs}, \bold{127} |
52 \item {\ptt addSIs}, \bold{116} |
52 \item {\tt addSIs}, \bold{123} |
53 \item {\ptt addSolver}, 98, 100 |
53 \item {\tt addSolver}, 104, 105 |
54 \item {\ptt addss}, 117, \bold{117}, 118 |
54 \item {\tt addss}, \bold{124}, 125 |
55 \item {\ptt addSSolver}, 98, 100 |
55 \item {\tt addSSolver}, 104, 105 |
56 \item {\ptt all_tac}, \bold{27} |
56 \item {\tt all_tac}, \bold{30} |
57 \item {\ptt ALLGOALS}, \bold{32}, 103, 106 |
57 \item {\tt ALLGOALS}, \bold{34}, 108, 112 |
58 \item ambiguity |
58 \item ambiguity |
59 \subitem of parsed expressions, 72 |
59 \subitem of parsed expressions, 75 |
60 \item {\ptt any} nonterminal, \bold{63} |
60 \item {\tt any} nonterminal, \bold{64} |
61 \item {\ptt APPEND}, \bold{26}, 27 |
61 \item {\tt APPEND}, \bold{28}, 30 |
62 \item {\ptt APPEND'}, 33 |
62 \item {\tt APPEND'}, 35 |
63 \item {\ptt Appl}, 76 |
63 \item {\tt Appl}, 79 |
64 \item {\ptt aprop} nonterminal, \bold{63} |
64 \item {\tt aprop} nonterminal, \bold{66} |
65 \item {\ptt ares_tac}, \bold{18} |
65 \item {\tt ares_tac}, \bold{19} |
66 \item {\ptt args} nonterminal, 85 |
66 \item {\tt args} nonterminal, 89 |
67 \item {\ptt Arith} theory, 105 |
67 \item {\tt Arith} theory, 111 |
68 \item arities |
68 \item arities |
69 \subitem context conditions, 48 |
69 \subitem context conditions, 52 |
70 \item {\ptt Asm_full_simp_tac}, \bold{95}, 100 |
70 \item {\tt Asm_full_simp_tac}, \bold{100}, 105 |
71 \item {\ptt asm_full_simp_tac}, 20, \bold{99}, 100, 104 |
71 \item {\tt asm_full_simp_tac}, 22, 105, \bold{106}, 109 |
72 \item {\ptt asm_rl} theorem, 19 |
72 \item {\tt asm_rl} theorem, 21 |
73 \item {\ptt Asm_simp_tac}, \bold{94}, 100 |
73 \item {\tt Asm_simp_tac}, \bold{100}, 105 |
74 \item {\ptt asm_simp_tac}, \bold{99}, 100, 102, 110 |
74 \item {\tt asm_simp_tac}, 105, \bold{106}, 107, 116 |
75 \item associative-commutative operators, 105 |
75 \item associative-commutative operators, 110 |
76 \item {\ptt assume}, \bold{40} |
76 \item {\tt assume}, \bold{42} |
77 \item {\ptt assume_ax}, 8, \bold{52} |
77 \item {\tt assume_ax}, 8, \bold{55} |
78 \item {\ptt assume_tac}, \bold{16}, 116 |
78 \item {\tt assume_tac}, \bold{17}, 122 |
79 \item {\ptt assumption}, \bold{43} |
79 \item {\tt assumption}, \bold{45} |
80 \item assumptions |
80 \item assumptions |
81 \subitem contradictory, 121 |
81 \subitem contradictory, 128 |
82 \subitem deleting, 20 |
82 \subitem deleting, 22 |
83 \subitem in simplification, 94, 98 |
83 \subitem in simplification, 99, 104 |
84 \subitem inserting, 18 |
84 \subitem inserting, 19 |
85 \subitem negated, 114 |
85 \subitem negated, 120 |
86 \subitem of main goal, 6, 8, 13 |
86 \subitem of main goal, 7--9, 14 |
87 \subitem reordering, 104 |
87 \subitem reordering, 109 |
88 \subitem rotating, 20 |
88 \subitem rotating, 22 |
89 \subitem substitution in, 91 |
89 \subitem substitution in, 96 |
90 \subitem tactics for, 16 |
90 \subitem tactics for, 17 |
91 \item ASTs, 76--80 |
91 \item ASTs, 79--84 |
92 \subitem made from parse trees, 77 |
92 \subitem made from parse trees, 80 |
93 \subitem made from terms, 79 |
93 \subitem made from terms, 82 |
94 \item {\ptt atac}, \bold{17} |
94 \item {\tt atac}, \bold{19} |
|
95 \item {\tt axclass} section, 51 |
|
96 \item axiomatic type class, 51 |
95 \item axioms |
97 \item axioms |
96 \subitem extracting, 51 |
98 \subitem extracting, 55 |
97 \item {\ptt axioms_of}, \bold{52} |
99 \item {\tt axioms_of}, \bold{56} |
98 |
100 |
99 \indexspace |
101 \indexspace |
100 |
102 |
101 \item {\ptt ba}, \bold{10} |
103 \item {\tt ba}, \bold{11} |
102 \item {\ptt back}, \bold{9} |
104 \item {\tt back}, \bold{9} |
103 \item batch execution, 11 |
105 \item batch execution, 12 |
104 \item {\ptt bd}, \bold{10} |
106 \item {\tt bd}, \bold{11} |
105 \item {\ptt bds}, \bold{10} |
107 \item {\tt bds}, \bold{11} |
106 \item {\ptt be}, \bold{10} |
108 \item {\tt be}, \bold{11} |
107 \item {\ptt bes}, \bold{10} |
109 \item {\tt bes}, \bold{11} |
108 \item {\ptt BEST_FIRST}, \bold{29}, 30 |
110 \item {\tt BEST_FIRST}, \bold{31}, 32 |
109 \item {\ptt Best_tac}, \bold{121} |
111 \item {\tt Best_tac}, \bold{127} |
110 \item {\ptt best_tac}, \bold{119} |
112 \item {\tt best_tac}, \bold{126} |
111 \item {\ptt beta_conversion}, \bold{41} |
113 \item {\tt beta_conversion}, \bold{43} |
112 \item {\ptt bicompose}, \bold{43} |
114 \item {\tt bicompose}, \bold{46} |
113 \item {\ptt bimatch_tac}, \bold{22} |
115 \item {\tt bimatch_tac}, \bold{23} |
114 \item {\ptt bind_thm}, 8, \bold{8}, 35 |
116 \item {\tt bind_thm}, \bold{8}, 9, 37 |
115 \item binders, \bold{72} |
117 \item binders, \bold{74} |
116 \item {\ptt biresolution}, \bold{43} |
118 \item {\tt biresolution}, \bold{45} |
117 \item {\ptt biresolve_tac}, \bold{22}, 121 |
119 \item {\tt biresolve_tac}, \bold{23}, 128 |
118 \item {\ptt Blast.depth_tac}, \bold{119} |
120 \item {\tt Blast.depth_tac}, \bold{125} |
119 \item {\ptt Blast.trace}, \bold{119} |
121 \item {\tt Blast.trace}, \bold{125} |
120 \item {\ptt Blast_tac}, \bold{121} |
122 \item {\tt Blast_tac}, \bold{127} |
121 \item {\ptt blast_tac}, \bold{119} |
123 \item {\tt blast_tac}, \bold{125} |
122 \item {\ptt Bound}, \bold{56}, 77, 79, 80 |
124 \item {\tt Bound}, \bold{57}, 80, 82, 83 |
123 \item {\ptt bound_hyp_subst_tac}, \bold{91} |
125 \item {\tt bound_hyp_subst_tac}, \bold{96} |
124 \item {\ptt br}, \bold{10} |
126 \item {\tt br}, \bold{11} |
125 \item {\ptt BREADTH_FIRST}, \bold{29} |
127 \item {\tt BREADTH_FIRST}, \bold{31} |
126 \item {\ptt brs}, \bold{10} |
128 \item {\tt brs}, \bold{11} |
127 \item {\ptt bw}, \bold{11} |
129 \item {\tt bw}, \bold{12} |
128 \item {\ptt bws}, \bold{11} |
130 \item {\tt bws}, \bold{12} |
129 \item {\ptt by}, \bold{7}, 9, 10, 14 |
131 \item {\tt by}, \bold{7}, 9, 10, 15 |
130 \item {\ptt byev}, \bold{7} |
132 \item {\tt byev}, \bold{7} |
131 |
133 |
132 \indexspace |
134 \indexspace |
133 |
135 |
134 \item {\ptt cd}, \bold{2}, 50 |
136 \item {\tt cd}, \bold{3}, 53 |
135 \item {\ptt cert_axm}, \bold{58} |
137 \item {\tt cert_axm}, \bold{59} |
136 \item {\ptt CHANGED}, \bold{28} |
138 \item {\tt CHANGED}, \bold{30} |
137 \item {\ptt chop}, \bold{9}, 13 |
139 \item {\tt chop}, \bold{9}, 13 |
138 \item {\ptt choplev}, \bold{9} |
140 \item {\tt choplev}, \bold{9} |
139 \item claset |
141 \item claset |
140 \subitem current, 120 |
142 \subitem current, 127 |
141 \item {\ptt claset} ML type, 116 |
143 \item {\tt claset} ML type, 122 |
142 \item classes |
144 \item classes |
143 \subitem context conditions, 48 |
145 \subitem context conditions, 52 |
144 \item classical reasoner, 112--122 |
146 \item classical reasoner, 118--129 |
145 \subitem setting up, 122 |
147 \subitem setting up, 128 |
146 \subitem tactics, 118 |
148 \subitem tactics, 124 |
147 \item classical sets, 115 |
149 \item classical sets, 122 |
148 \item {\ptt ClassicalFun}, 122 |
150 \item {\tt ClassicalFun}, 129 |
149 \item {\ptt combination}, \bold{41} |
151 \item {\tt combination}, \bold{44} |
150 \item {\ptt commit}, \bold{2} |
152 \item {\tt commit}, \bold{2} |
151 \item {\ptt COMP}, \bold{43} |
153 \item {\tt COMP}, \bold{46} |
152 \item {\ptt compose}, \bold{43} |
154 \item {\tt compose}, \bold{46} |
153 \item {\ptt compose_tac}, \bold{21} |
155 \item {\tt compose_tac}, \bold{22} |
154 \item {\ptt compSWrapper}, \bold{118} |
156 \item {\tt compSWrapper}, \bold{124} |
155 \item {\ptt compWrapper}, \bold{118} |
157 \item {\tt compWrapper}, \bold{124} |
156 \item {\ptt concl_of}, \bold{37} |
158 \item {\tt concl_of}, \bold{39} |
157 \item {\ptt COND}, \bold{30} |
159 \item {\tt COND}, \bold{32} |
158 \item congruence rules, 97 |
160 \item congruence rules, 102 |
159 \item {\ptt Const}, \bold{56}, 79, 88 |
161 \item {\tt Const}, \bold{57}, 82, 92 |
160 \item {\ptt Constant}, 76, 88 |
162 \item {\tt Constant}, 79, 92 |
161 \item constants, \bold{56} |
163 \item constants, \bold{57} |
162 \subitem for translations, 68 |
164 \subitem for translations, 69 |
163 \subitem syntactic, 81 |
165 \subitem syntactic, 84 |
164 \item {\ptt contr_tac}, \bold{121} |
166 \item {\tt contr_tac}, \bold{128} |
165 \item {\ptt could_unify}, \bold{23} |
167 \item {\tt could_unify}, \bold{24} |
166 \item {\ptt cterm} ML type, 58 |
168 \item {\tt CPure} theory, 49 |
167 \item {\ptt cterm_instantiate}, \bold{36} |
169 \item {\tt CPure.thy}, \bold{55} |
168 \item {\ptt cterm_of}, \bold{58} |
170 \item {\tt cterm} ML type, 59 |
169 \item {\ptt ctyp}, \bold{59} |
171 \item {\tt cterm_instantiate}, \bold{38} |
170 \item {\ptt ctyp_of}, \bold{59} |
172 \item {\tt cterm_of}, 7, 13, \bold{59} |
171 \item {\ptt cut_facts_tac}, 7, \bold{18}, 92 |
173 \item {\tt ctyp}, \bold{60} |
172 \item {\ptt cut_inst_tac}, \bold{18} |
174 \item {\tt ctyp_of}, \bold{61} |
173 \item {\ptt cut_rl} theorem, 19 |
175 \item {\tt cut_facts_tac}, 7, \bold{19}, 97 |
174 |
176 \item {\tt cut_inst_tac}, \bold{19} |
175 \indexspace |
177 \item {\tt cut_rl} theorem, 21 |
176 |
178 |
177 \item {\ptt datatype}, 95 |
179 \indexspace |
178 \item {\ptt Deepen_tac}, \bold{121} |
180 |
179 \item {\ptt deepen_tac}, \bold{120} |
181 \item {\tt datatype}, 100 |
180 \item {\ptt defer_tac}, \bold{18} |
182 \item {\tt Deepen_tac}, \bold{127} |
181 \item definitions, \see{rewriting, meta-level}{0}, 18, \bold{48} |
183 \item {\tt deepen_tac}, \bold{126} |
|
184 \item {\tt defer_tac}, \bold{20} |
|
185 \item definitions, \see{rewriting, meta-level}{1}, 20, \bold{51} |
182 \subitem unfolding, 7, 8 |
186 \subitem unfolding, 7, 8 |
183 \item {\ptt delcongs}, 97 |
187 \item {\tt delcongs}, 103 |
184 \item {\ptt deleqcongs}, 97, 100 |
188 \item {\tt deleqcongs}, 103, 105 |
185 \item {\ptt delete_tmpfiles}, \bold{49} |
189 \item {\tt delete_tmpfiles}, \bold{53} |
186 \item delimiters, \bold{65}, 67, 68, 70 |
190 \item delimiters, \bold{66}, 69, 70, 72 |
187 \item {\ptt delrules}, \bold{116} |
191 \item {\tt delrules}, \bold{123} |
188 \item {\ptt Delsimps}, \bold{95}, 99, 100 |
192 \item {\tt Delsimps}, \bold{100}, 105, 106 |
189 \item {\ptt delsimps}, 99, 100 |
193 \item {\tt delsimps}, 105, 106 |
190 \item {\ptt dependent_tr'}, 86, \bold{88} |
194 \item {\tt dependent_tr'}, 90, \bold{92} |
191 \item {\ptt DEPTH_FIRST}, \bold{29} |
195 \item {\tt DEPTH_FIRST}, \bold{31} |
192 \item {\ptt DEPTH_SOLVE}, \bold{29} |
196 \item {\tt DEPTH_SOLVE}, \bold{31} |
193 \item {\ptt DEPTH_SOLVE_1}, \bold{29} |
197 \item {\tt DEPTH_SOLVE_1}, \bold{31} |
194 \item {\ptt depth_tac}, \bold{120} |
198 \item {\tt depth_tac}, \bold{126} |
195 \item {\ptt Deriv.drop}, \bold{45} |
199 \item {\tt Deriv.drop}, \bold{48} |
196 \item {\ptt Deriv.linear}, \bold{45} |
200 \item {\tt Deriv.linear}, \bold{48} |
197 \item {\ptt Deriv.size}, \bold{45} |
201 \item {\tt Deriv.size}, \bold{48} |
198 \item {\ptt Deriv.tree}, \bold{45} |
202 \item {\tt Deriv.tree}, \bold{48} |
199 \item {\ptt dest_eq}, \bold{92} |
203 \item {\tt dest_eq}, \bold{97} |
200 \item {\ptt dest_state}, \bold{37} |
204 \item {\tt dest_state}, \bold{39} |
201 \item destruct-resolution, 15 |
205 \item destruct-resolution, 17 |
202 \item {\ptt DETERM}, \bold{30} |
206 \item {\tt DETERM}, \bold{32} |
203 \item discrimination nets, \bold{22} |
207 \item discrimination nets, \bold{24} |
204 \item {\ptt dmatch_tac}, \bold{16} |
208 \item {\tt dmatch_tac}, \bold{17} |
205 \item {\ptt dres_inst_tac}, \bold{17} |
209 \item {\tt dres_inst_tac}, \bold{18} |
206 \item {\ptt dresolve_tac}, \bold{15} |
210 \item {\tt dresolve_tac}, \bold{17} |
207 \item {\ptt dtac}, \bold{17} |
211 \item {\tt dtac}, \bold{19} |
208 \item {\ptt dummyT}, 79, 80, 89 |
212 \item {\tt dummyT}, 82, 83, 93 |
209 |
213 |
210 \indexspace |
214 \indexspace |
211 |
215 |
212 \item elim-resolution, 15 |
216 \item elim-resolution, 16 |
213 \item {\ptt ematch_tac}, \bold{16} |
217 \item {\tt ematch_tac}, \bold{17} |
214 \item {\ptt empty} constant, 85 |
218 \item {\tt empty} constant, 88 |
215 \item {\ptt empty_cs}, \bold{116} |
219 \item {\tt empty_cs}, \bold{122} |
216 \item {\ptt empty_ss}, 100, 110 |
220 \item {\tt empty_ss}, 105, 116 |
217 \item {\ptt eq_assume_tac}, \bold{16}, 116 |
221 \item {\tt eq_assume_tac}, \bold{17}, 122 |
218 \item {\ptt eq_assumption}, \bold{43} |
222 \item {\tt eq_assumption}, \bold{45} |
219 \item {\ptt eq_mp_tac}, \bold{121} |
223 \item {\tt eq_mp_tac}, \bold{128} |
220 \item {\ptt eq_reflection} theorem, \bold{92}, 107 |
224 \item {\tt eq_reflection} theorem, \bold{97}, 113 |
221 \item {\ptt eq_thm}, \bold{30} |
225 \item {\tt eq_thm}, \bold{32} |
222 \item {\ptt equal_elim}, \bold{41} |
226 \item {\tt equal_elim}, \bold{43} |
223 \item {\ptt equal_intr}, \bold{40} |
227 \item {\tt equal_intr}, \bold{43} |
224 \item equality, 90--93 |
228 \item equality, 95--98 |
225 \item {\ptt eres_inst_tac}, \bold{17} |
229 \item {\tt eres_inst_tac}, \bold{18} |
226 \item {\ptt eresolve_tac}, \bold{15} |
230 \item {\tt eresolve_tac}, \bold{16} |
227 \item {\ptt eta_contract}, \bold{4}, 83 |
231 \item {\tt eta_contract}, \bold{4}, 86 |
228 \item {\ptt etac}, \bold{17} |
232 \item {\tt etac}, \bold{19} |
229 \item {\ptt EVERY}, \bold{27} |
233 \item {\tt EVERY}, \bold{29} |
230 \item {\ptt EVERY'}, 33 |
234 \item {\tt EVERY'}, 35 |
231 \item {\ptt EVERY1}, \bold{33} |
235 \item {\tt EVERY1}, \bold{35} |
232 \item examples |
236 \item examples |
233 \subitem of logic definitions, 73 |
237 \subitem of logic definitions, 76 |
234 \subitem of macros, 85, 86 |
238 \subitem of macros, 88, 89 |
235 \subitem of mixfix declarations, 70 |
239 \subitem of mixfix declarations, 71 |
236 \subitem of simplification, 101 |
240 \subitem of simplification, 106 |
237 \subitem of translations, 88 |
241 \subitem of translations, 92 |
238 \item exceptions |
242 \item exceptions |
239 \subitem printing of, 4 |
243 \subitem printing of, 4 |
240 \item {\ptt expandshort} shell script, 5 |
244 \item {\tt exit}, \bold{2} |
241 \item {\ptt exportML}, \bold{2} |
245 \item {\tt extensional}, \bold{44} |
242 \item {\ptt extensional}, \bold{41} |
246 |
243 |
247 \indexspace |
244 \indexspace |
248 |
245 |
249 \item {\tt fa}, \bold{11} |
246 \item {\ptt fa}, \bold{11} |
250 \item {\tt Fast_tac}, \bold{127} |
247 \item {\ptt Fast_tac}, \bold{121} |
251 \item {\tt fast_tac}, \bold{126} |
248 \item {\ptt fast_tac}, \bold{119} |
252 \item {\tt fd}, \bold{11} |
249 \item {\ptt fd}, \bold{11} |
253 \item {\tt fds}, \bold{11} |
250 \item {\ptt fds}, \bold{11} |
254 \item {\tt fe}, \bold{11} |
251 \item {\ptt fe}, \bold{11} |
255 \item {\tt fes}, \bold{11} |
252 \item {\ptt fes}, \bold{11} |
|
253 \item files |
256 \item files |
254 \subitem reading, 2, 49 |
257 \subitem reading, 3, 52 |
255 \item {\ptt filt_resolve_tac}, \bold{23} |
258 \item {\tt filt_resolve_tac}, \bold{24} |
256 \item {\ptt FILTER}, \bold{28} |
259 \item {\tt FILTER}, \bold{30} |
257 \item {\ptt filter_goal}, \bold{14} |
260 \item {\tt filter_goal}, \bold{15} |
258 \item {\ptt filter_thms}, \bold{23} |
261 \item {\tt filter_thms}, \bold{25} |
259 \item {\ptt findE}, \bold{9} |
262 \item {\tt findE}, \bold{9} |
260 \item {\ptt findEs}, \bold{9} |
263 \item {\tt findEs}, \bold{9} |
261 \item {\ptt findI}, \bold{8} |
264 \item {\tt findI}, \bold{9} |
262 \item {\ptt finish_html}, \bold{54} |
265 \item {\tt FIRST}, \bold{29} |
263 \item {\ptt FIRST}, \bold{27} |
266 \item {\tt FIRST'}, 35 |
264 \item {\ptt FIRST'}, 33 |
267 \item {\tt FIRST1}, \bold{35} |
265 \item {\ptt FIRST1}, \bold{33} |
268 \item {\tt FIRSTGOAL}, \bold{34} |
266 \item {\ptt FIRSTGOAL}, \bold{32} |
269 \item flex-flex constraints, 22, 39, 47 |
267 \item flex-flex constraints, 20, 37, 44 |
270 \item {\tt flexflex_rule}, \bold{47} |
268 \item {\ptt flexflex_rule}, \bold{44} |
271 \item {\tt flexflex_tac}, \bold{22} |
269 \item {\ptt flexflex_tac}, \bold{21} |
272 \item {\tt fold_goals_tac}, \bold{20} |
270 \item {\ptt fold_goals_tac}, \bold{19} |
273 \item {\tt fold_tac}, \bold{20} |
271 \item {\ptt fold_tac}, \bold{19} |
274 \item {\tt forall_elim}, \bold{44} |
272 \item {\ptt forall_elim}, \bold{42} |
275 \item {\tt forall_elim_list}, \bold{44} |
273 \item {\ptt forall_elim_list}, \bold{42} |
276 \item {\tt forall_elim_var}, \bold{44} |
274 \item {\ptt forall_elim_var}, \bold{42} |
277 \item {\tt forall_elim_vars}, \bold{45} |
275 \item {\ptt forall_elim_vars}, \bold{42} |
278 \item {\tt forall_intr}, \bold{44} |
276 \item {\ptt forall_intr}, \bold{41} |
279 \item {\tt forall_intr_frees}, \bold{44} |
277 \item {\ptt forall_intr_frees}, \bold{42} |
280 \item {\tt forall_intr_list}, \bold{44} |
278 \item {\ptt forall_intr_list}, \bold{42} |
281 \item {\tt force_strip_shyps}, \bold{40} |
279 \item {\ptt force_strip_shyps}, \bold{37} |
282 \item {\tt forw_inst_tac}, \bold{18} |
280 \item {\ptt forw_inst_tac}, \bold{17} |
283 \item forward proof, 17, 37 |
281 \item forward proof, 15, 16, 35 |
284 \item {\tt forward_tac}, \bold{17} |
282 \item {\ptt forward_tac}, \bold{16} |
285 \item {\tt fr}, \bold{11} |
283 \item {\ptt fr}, \bold{11} |
286 \item {\tt Free}, \bold{57}, 82 |
284 \item {\ptt Free}, \bold{56}, 79 |
287 \item {\tt freezeT}, \bold{45} |
285 \item {\ptt freezeT}, \bold{42} |
288 \item {\tt frs}, \bold{11} |
286 \item {\ptt frs}, \bold{11} |
289 \item {\tt Full_simp_tac}, \bold{100}, 105 |
287 \item {\ptt Full_simp_tac}, \bold{94}, 100 |
290 \item {\tt full_simp_tac}, 105, \bold{106} |
288 \item {\ptt full_simp_tac}, \bold{99}, 100 |
291 \item {\tt fun} type, 60 |
289 \item {\ptt fun} type, 59 |
292 \item function applications, \bold{57} |
290 \item function applications, \bold{56} |
293 |
291 |
294 \indexspace |
292 \indexspace |
295 |
293 |
296 \item {\tt get_axiom}, \bold{55} |
294 \item {\ptt get_axiom}, \bold{51} |
297 \item {\tt get_thm}, \bold{55} |
295 \item {\ptt get_thm}, \bold{51} |
298 \item {\tt getgoal}, \bold{15} |
296 \item {\ptt getgoal}, \bold{14} |
299 \item {\tt gethyps}, \bold{15}, 33 |
297 \item {\ptt gethyps}, \bold{14}, 31 |
300 \item {\tt goal}, \bold{7}, 13 |
298 \item {\ptt goal}, \bold{7}, 13 |
301 \item {\tt goals_limit}, \bold{10} |
299 \item {\ptt goals_limit}, \bold{10} |
302 \item {\tt goalw}, \bold{7} |
300 \item {\ptt goalw}, \bold{7} |
303 \item {\tt goalw_cterm}, \bold{7} |
301 \item {\ptt goalw_cterm}, \bold{7} |
304 |
302 |
305 \indexspace |
303 \indexspace |
306 |
304 |
307 \item {\tt has_fewer_prems}, \bold{32} |
305 \item {\ptt has_fewer_prems}, \bold{30} |
308 \item {\tt hyp_subst_tac}, \bold{96} |
306 \item HTML, \bold{53} |
309 \item {\tt hyp_subst_tacs}, \bold{129} |
307 \item {\ptt hyp_subst_tac}, \bold{91} |
310 \item {\tt HypsubstFun}, 97, 129 |
308 \item {\ptt hyp_subst_tacs}, \bold{122} |
311 |
309 \item {\ptt HypsubstFun}, 92, 122 |
312 \indexspace |
310 |
313 |
311 \indexspace |
314 \item {\tt id} nonterminal, \bold{66}, 80, 87 |
312 |
315 \item identifiers, 66 |
313 \item {\ptt id} nonterminal, \bold{65}, 77, 84 |
316 \item {\tt idt} nonterminal, 86 |
314 \item identifiers, 65 |
317 \item {\tt idts} nonterminal, \bold{66}, 74 |
315 \item {\ptt idt} nonterminal, 83 |
318 \item {\tt IF_UNSOLVED}, \bold{32} |
316 \item {\ptt idts} nonterminal, \bold{65}, 72 |
319 \item {\tt iff_reflection} theorem, 113 |
317 \item {\ptt IF_UNSOLVED}, \bold{30} |
320 \item {\tt imp_intr} theorem, \bold{97} |
318 \item {\ptt iff_reflection} theorem, 107 |
321 \item {\tt implies_elim}, \bold{43} |
319 \item {\ptt imp_intr} theorem, \bold{92} |
322 \item {\tt implies_elim_list}, \bold{43} |
320 \item {\ptt implies_elim}, \bold{40} |
323 \item {\tt implies_intr}, \bold{42} |
321 \item {\ptt implies_elim_list}, \bold{40} |
324 \item {\tt implies_intr_hyps}, \bold{43} |
322 \item {\ptt implies_intr}, \bold{40} |
325 \item {\tt implies_intr_list}, \bold{42} |
323 \item {\ptt implies_intr_hyps}, \bold{40} |
326 \item {\tt incr_boundvars}, \bold{58}, 92 |
324 \item {\ptt implies_intr_list}, \bold{40} |
327 \item {\tt indexname} ML type, 57, 67 |
325 \item {\ptt incr_boundvars}, \bold{57}, 88 |
328 \item infixes, \bold{73} |
326 \item {\ptt indexname} ML type, 56, 66 |
329 \item {\tt insert} constant, 88 |
327 \item infixes, \bold{71} |
330 \item {\tt inst_step_tac}, \bold{127} |
328 \item {\ptt init_html}, \bold{54} |
331 \item {\tt instance} section, 51 |
329 \item {\ptt insert} constant, 85 |
332 \item {\tt instantiate}, \bold{45} |
330 \item {\ptt inst_step_tac}, \bold{120} |
333 \item instantiation, 17, 38, 45 |
331 \item {\ptt instantiate}, \bold{42} |
334 \item {\tt INTLEAVE}, \bold{28}, 30 |
332 \item instantiation, 16, 36, 42 |
335 \item {\tt INTLEAVE'}, 35 |
333 \item {\ptt INTLEAVE}, \bold{26}, 27 |
336 \item {\tt invoke_oracle}, \bold{61} |
334 \item {\ptt INTLEAVE'}, 33 |
337 \item {\tt is} nonterminal, 88 |
335 \item {\ptt invoke_oracle}, \bold{60} |
338 |
336 \item {\ptt is} nonterminal, 85 |
339 \indexspace |
337 |
340 |
338 \indexspace |
341 \item {\tt joinrules}, \bold{128} |
339 |
342 |
340 \item {\ptt joinrules}, \bold{121} |
343 \indexspace |
341 |
344 |
342 \indexspace |
345 \item {\tt keep_derivs}, \bold{48} |
343 |
346 |
344 \item {\ptt keep_derivs}, \bold{45} |
347 \indexspace |
345 |
348 |
346 \indexspace |
349 \item $\lambda$-abstractions, 24, \bold{57} |
347 |
350 \item $\lambda$-calculus, 42, 43, 66 |
348 \item $\lambda$-abstractions, 22, \bold{56} |
351 \item {\tt lessb}, \bold{23} |
349 \item $\lambda$-calculus, 39, 41, 65 |
352 \item lexer, \bold{66} |
350 \item {\ptt lessb}, \bold{22} |
353 \item {\tt lift_rule}, \bold{46} |
351 \item lexer, \bold{65} |
354 \item lifting, 46 |
352 \item {\ptt lift_rule}, \bold{44} |
355 \item {\tt loadpath}, \bold{53} |
353 \item lifting, 44 |
356 \item {\tt logic} class, 66, 71 |
354 \item {\ptt loadpath}, \bold{49} |
357 \item {\tt logic} nonterminal, \bold{66} |
355 \item {\ptt logic} class, 63, 65, 69 |
358 \item {\tt Logic.auto_rename}, \bold{21} |
356 \item {\ptt logic} nonterminal, \bold{63} |
359 \item {\tt Logic.set_rename_prefix}, \bold{21} |
357 \item {\ptt Logic.auto_rename}, \bold{20} |
360 \item {\tt loose_bnos}, \bold{58}, 93 |
358 \item {\ptt Logic.set_rename_prefix}, \bold{20} |
361 |
359 \item {\ptt loose_bnos}, \bold{57}, 89 |
362 \indexspace |
360 |
363 |
361 \indexspace |
364 \item macros, 84--90 |
362 |
365 \item {\tt make_elim}, \bold{39}, 123 |
363 \item macros, 81--86 |
366 \item {\tt Match} exception, 91, 97 |
364 \item {\ptt make-all} shell script, 5 |
367 \item {\tt match_tac}, \bold{17}, 122 |
365 \item {\ptt make_elim}, \bold{37}, 117 |
368 \item {\tt max_pri}, 64, \bold{70} |
366 \item {\ptt make_html}, \bold{54} |
369 \item {\tt merge_ss}, 105 |
367 \item {\ptt Match} exception, 88, 92 |
370 \item {\tt merge_theories}, \bold{55} |
368 \item {\ptt match_tac}, \bold{16}, 116 |
371 \item meta-assumptions, 33, 41, 42, 45 |
369 \item {\ptt max_pri}, 63, \bold{69} |
372 \subitem printing of, 4 |
370 \item {\ptt merge_ss}, 100 |
373 \item meta-equality, 41, 43 |
371 \item {\ptt merge_theories}, \bold{52}, \fnote{75} |
374 \item meta-implication, 41, 42 |
372 \item meta-assumptions, 31, 39, 40, 43 |
375 \item meta-quantifiers, 42, 44 |
373 \subitem printing of, 3 |
376 \item meta-rewriting, 7, 12, 13, \bold{20}, |
374 \item meta-equality, 39--41 |
377 \seealso{tactics, theorems}{130} |
375 \item meta-implication, 39, 40 |
378 \subitem in terms, 47 |
376 \item meta-quantifiers, 40, 41 |
379 \subitem in theorems, 38 |
377 \item meta-rewriting, 7, 11, 12, \bold{18}, |
380 \item meta-rules, \see{meta-rules}{1}, 41--47 |
378 \seealso{tactics, theorems}{123} |
381 \item {\tt METAHYPS}, 15, \bold{33} |
379 \subitem in terms, 44 |
382 \item mixfix declarations, 50, 69--74 |
380 \subitem in theorems, 35 |
383 \item {\tt mk_case_split_tac}, \bold{116} |
381 \item meta-rules, \see{meta-rules}{0}, 39--44 |
384 \item {\tt ML} section, 51, 91, 93 |
382 \item {\ptt METAHYPS}, 14, \bold{31} |
385 \item {\tt mp} theorem, \bold{129} |
383 \item mixfix declarations, 47, 68--72 |
386 \item {\tt mp_tac}, \bold{128} |
384 \item {\ptt mk_case_split_tac}, \bold{111} |
387 \item {\tt MRL}, \bold{37} |
385 \item {\ptt ML} section, 48, 87, 89 |
388 \item {\tt MRS}, \bold{37} |
386 \item {\ptt mp} theorem, \bold{122} |
389 |
387 \item {\ptt mp_tac}, \bold{121} |
390 \indexspace |
388 \item {\ptt MRL}, \bold{35} |
391 |
389 \item {\ptt MRS}, \bold{35} |
392 \item name tokens, \bold{66} |
390 |
393 \item {\tt net_bimatch_tac}, \bold{24} |
391 \indexspace |
394 \item {\tt net_biresolve_tac}, \bold{24} |
392 |
395 \item {\tt net_match_tac}, \bold{24} |
393 \item name tokens, \bold{65} |
396 \item {\tt net_resolve_tac}, \bold{24} |
394 \item {\ptt net_bimatch_tac}, \bold{23} |
397 \item {\tt no_tac}, \bold{30} |
395 \item {\ptt net_biresolve_tac}, \bold{23} |
398 \item {\tt None}, \bold{26} |
396 \item {\ptt net_match_tac}, \bold{23} |
399 \item {\tt not_elim} theorem, \bold{129} |
397 \item {\ptt net_resolve_tac}, \bold{22} |
400 \item {\tt nprems_of}, \bold{39} |
398 \item {\ptt no_tac}, \bold{27} |
401 \item numerals, 66 |
399 \item {\ptt None}, \bold{24} |
402 |
400 \item {\ptt not_elim} theorem, \bold{122} |
403 \indexspace |
401 \item {\ptt nprems_of}, \bold{37} |
404 |
402 \item numerals, 65 |
405 \item {\tt o} type, 76 |
403 |
406 \item {\tt op} symbol, 73 |
404 \indexspace |
407 \item {\tt option} ML type, 26 |
405 |
408 \item oracles, 61--62 |
406 \item {\ptt o} type, 73 |
409 \item {\tt ORELSE}, \bold{28}, 30, 34 |
407 \item {\ptt op} symbol, 71 |
410 \item {\tt ORELSE'}, 35 |
408 \item {\ptt option} ML type, 24 |
|
409 \item oracles, 60--61 |
|
410 \item {\ptt ORELSE}, \bold{26}, 27, 28, 32 |
|
411 \item {\ptt ORELSE'}, 33 |
|
412 |
411 |
413 \indexspace |
412 \indexspace |
414 |
413 |
415 \item parameters |
414 \item parameters |
416 \subitem removing unused, 20 |
415 \subitem removing unused, 22 |
417 \subitem renaming, 11, 19, 44 |
416 \subitem renaming, 12, 21, 47 |
418 \item {\ptt parents_of}, \bold{52} |
417 \item {\tt parents_of}, \bold{56} |
419 \item parse trees, 76 |
418 \item parse trees, 79 |
420 \item {\ptt parse_ast_translation}, 87 |
419 \item {\tt parse_ast_translation}, 91 |
421 \item {\ptt parse_rules}, 83 |
420 \item {\tt parse_rules}, 86 |
422 \item {\ptt parse_translation}, 87 |
421 \item {\tt parse_translation}, 91 |
423 \item {\ptt pause_tac}, \bold{24} |
422 \item {\tt pause_tac}, \bold{26} |
424 \item Poly/{\ML} compiler, 1, 2, 4, 50 |
423 \item Poly/{\ML} compiler, 5 |
425 \item {\ptt pop_proof}, \bold{13} |
424 \item {\tt pop_proof}, \bold{14} |
426 \item {\ptt pr}, \bold{10} |
425 \item {\tt pr}, \bold{10} |
427 \item {\ptt premises}, \bold{7}, 13 |
426 \item {\tt premises}, \bold{7}, 14 |
428 \item {\ptt prems_of}, \bold{37} |
427 \item {\tt prems_of}, \bold{39} |
429 \item {\ptt prems_of_ss}, 100 |
428 \item {\tt prems_of_ss}, 105 |
430 \item pretty printing, 68, 71, 85 |
429 \item pretty printing, 70, 72--73, 89 |
431 \item {\ptt Pretty.setdepth}, \bold{3} |
430 \item {\tt Pretty.setdepth}, \bold{3} |
432 \item {\ptt Pretty.setmargin}, \bold{3} |
431 \item {\tt Pretty.setmargin}, \bold{3} |
433 \item {\ptt PRIMITIVE}, \bold{24} |
432 \item {\tt PRIMITIVE}, \bold{25} |
434 \item {\ptt primrec}, 95 |
433 \item {\tt primrec}, 100 |
435 \item {\ptt prin}, 4, \bold{14} |
434 \item {\tt prin}, 5, \bold{14} |
436 \item {\ptt print_ast_translation}, 87 |
435 \item print mode, 50, 93 |
437 \item {\ptt print_cs}, \bold{116} |
436 \item print modes, 74--75 |
438 \item {\ptt print_depth}, \bold{3} |
437 \item {\tt print_ast_translation}, 91 |
439 \item {\ptt print_exn}, \bold{4}, 34 |
438 \item {\tt print_cs}, \bold{122} |
440 \item {\ptt print_goals}, \bold{35} |
439 \item {\tt print_depth}, \bold{4} |
441 \item {\ptt print_rules}, 83 |
440 \item {\tt print_exn}, \bold{5}, 36 |
442 \item {\ptt print_syntax}, \bold{66} |
441 \item {\tt print_goals}, \bold{37} |
443 \item {\ptt print_tac}, \bold{24} |
442 \item {\tt print_mode}, 74 |
444 \item {\ptt print_theory}, \bold{52} |
443 \item {\tt print_modes}, 69 |
445 \item {\ptt print_thm}, \bold{35} |
444 \item {\tt print_rules}, 86 |
446 \item {\ptt print_translation}, 87 |
445 \item {\tt print_syntax}, \bold{56}, \bold{68} |
|
446 \item {\tt print_tac}, \bold{26} |
|
447 \item {\tt print_theory}, \bold{56} |
|
448 \item {\tt print_thm}, \bold{37} |
|
449 \item {\tt print_translation}, 91 |
447 \item printing control, 3--4 |
450 \item printing control, 3--4 |
448 \item {\ptt printyp}, \bold{14} |
451 \item {\tt printyp}, \bold{14} |
449 \item priorities, 62, \bold{69} |
452 \item priorities, 63, \bold{70} |
450 \item priority grammars, 62--63 |
453 \item priority grammars, 63--64 |
451 \item {\ptt prlev}, \bold{10} |
454 \item {\tt prlev}, \bold{10} |
452 \item {\ptt prlim}, \bold{10} |
455 \item {\tt prlim}, \bold{10} |
453 \item productions, 62, 67, 68 |
456 \item productions, 63, 69, 70 |
454 \subitem copy, \bold{67}, 68, 77 |
457 \subitem copy, \bold{69}, 70, 81 |
455 \item {\ptt proof} ML type, 13 |
458 \item {\tt proof} ML type, 14 |
456 \item proof objects, 44--45 |
459 \item proof objects, 47--48 |
457 \item proof state, 6 |
460 \item proof state, 6 |
458 \subitem printing of, 9 |
461 \subitem printing of, 10 |
459 \item {\ptt proof_timing}, \bold{10} |
462 \item {\tt proof_timing}, \bold{10} |
460 \item proofs, 6--14 |
463 \item proofs, 6--15 |
461 \subitem inspecting the state, 14 |
464 \subitem inspecting the state, 15 |
462 \subitem managing multiple, 12 |
465 \subitem managing multiple, 13 |
463 \subitem saving and restoring, 13 |
466 \subitem saving and restoring, 14 |
464 \subitem stacking, 13 |
467 \subitem stacking, 13 |
465 \subitem starting, 6 |
468 \subitem starting, 6 |
466 \subitem timing, 10 |
469 \subitem timing, 10 |
467 \item {\ptt PROP} symbol, 64 |
470 \item {\tt PROP} symbol, 65 |
468 \item {\ptt prop} nonterminal, \bold{63}, 73 |
471 \item {\tt prop} nonterminal, \bold{64}, 76 |
469 \item {\ptt prop} type, 59, 63 |
472 \item {\tt prop} type, 60, 66 |
470 \item {\ptt prove_goal}, 10, \bold{12} |
473 \item {\tt prove_goal}, 10, \bold{12} |
471 \item {\ptt prove_goalw}, \bold{12} |
474 \item {\tt prove_goalw}, \bold{13} |
472 \item {\ptt prove_goalw_cterm}, \bold{12} |
475 \item {\tt prove_goalw_cterm}, \bold{13} |
473 \item {\ptt prth}, \bold{34} |
476 \item {\tt prth}, \bold{36} |
474 \item {\ptt prthq}, \bold{35} |
477 \item {\tt prthq}, \bold{37} |
475 \item {\ptt prths}, \bold{34} |
478 \item {\tt prths}, \bold{37} |
476 \item {\ptt prune_params_tac}, \bold{21} |
479 \item {\tt prune_params_tac}, \bold{22} |
477 \item {\ptt Pure} theory, 46, 63, 67 |
480 \item {\tt Pure} theory, 49, 64, 68 |
478 \item {\ptt pure_thy}, \bold{52} |
481 \item {\tt Pure.thy}, \bold{55} |
479 \item {\ptt push_proof}, \bold{13} |
482 \item {\tt push_proof}, \bold{14} |
480 \item {\ptt pwd}, \bold{2} |
483 \item {\tt pwd}, \bold{3} |
481 |
484 |
482 \indexspace |
485 \indexspace |
483 |
486 |
484 \item {\ptt qed}, 8, \bold{8} |
487 \item {\tt qed}, \bold{8}, 9 |
485 \item {\ptt qed_goal}, \bold{12} |
488 \item {\tt qed_goal}, \bold{13} |
486 \item {\ptt qed_goalw}, \bold{12} |
489 \item {\tt qed_goalw}, \bold{13} |
487 \item quantifiers, 72 |
490 \item quantifiers, 74 |
488 \item {\ptt quit}, \bold{2} |
491 \item {\tt quit}, \bold{2} |
489 |
492 |
490 \indexspace |
493 \indexspace |
491 |
494 |
492 \item {\ptt read}, \bold{14} |
495 \item {\tt read}, \bold{14} |
493 \item {\ptt read_axm}, \bold{58} |
496 \item {\tt read_axm}, \bold{59} |
494 \item {\ptt read_cterm}, \bold{58} |
497 \item {\tt read_cterm}, \bold{59} |
495 \item {\ptt read_instantiate}, \bold{36} |
498 \item {\tt read_instantiate}, \bold{38} |
496 \item {\ptt read_instantiate_sg}, \bold{36} |
499 \item {\tt read_instantiate_sg}, \bold{38} |
497 \item reading |
500 \item reading |
498 \subitem axioms, \see{{\tt assume_ax}}{46} |
501 \subitem axioms, \see{{\tt assume_ax}}{49} |
499 \subitem goals, \see{proofs, starting}{6} |
502 \subitem goals, \see{proofs, starting}{6} |
500 \item {\ptt reflexive}, \bold{41} |
503 \item {\tt reflexive}, \bold{43} |
501 \item {\ptt ren}, \bold{11} |
504 \item {\tt ren}, \bold{12} |
502 \item {\ptt rename_last_tac}, \bold{20} |
505 \item {\tt rename_last_tac}, \bold{21} |
503 \item {\ptt rename_params_rule}, \bold{44} |
506 \item {\tt rename_params_rule}, \bold{46} |
504 \item {\ptt rename_tac}, \bold{20} |
507 \item {\tt rename_tac}, \bold{21} |
505 \item {\ptt rep_cterm}, \bold{58} |
508 \item {\tt rep_cterm}, \bold{59} |
506 \item {\ptt rep_ctyp}, \bold{59} |
509 \item {\tt rep_ctyp}, \bold{61} |
507 \item {\ptt rep_ss}, 100 |
510 \item {\tt rep_ss}, 105 |
508 \item {\ptt rep_thm}, \bold{37} |
511 \item {\tt rep_thm}, \bold{40} |
509 \item {\ptt REPEAT}, \bold{27, 28} |
512 \item {\tt REPEAT}, \bold{29, 30} |
510 \item {\ptt REPEAT1}, \bold{27} |
513 \item {\tt REPEAT1}, \bold{29} |
511 \item {\ptt REPEAT_DETERM}, \bold{27} |
514 \item {\tt REPEAT_DETERM}, \bold{29} |
512 \item {\ptt REPEAT_FIRST}, \bold{32} |
515 \item {\tt REPEAT_FIRST}, \bold{34} |
513 \item {\ptt REPEAT_SOME}, \bold{32} |
516 \item {\tt REPEAT_SOME}, \bold{34} |
514 \item {\ptt res_inst_tac}, \bold{17}, 21 |
517 \item {\tt res_inst_tac}, \bold{18}, 22 |
515 \item reserved words, 65, 86 |
518 \item reserved words, 66, 89 |
516 \item resolution, 35, 43 |
519 \item {\tt reset}, 3 |
517 \subitem tactics, 15 |
520 \item resolution, 37, 45 |
518 \subitem without lifting, 43 |
521 \subitem tactics, 16 |
519 \item {\ptt resolve_tac}, \bold{15}, 116 |
522 \subitem without lifting, 46 |
520 \item {\ptt restore_proof}, \bold{13} |
523 \item {\tt resolve_tac}, \bold{16}, 122 |
521 \item {\ptt result}, \bold{8}, 14, 52 |
524 \item {\tt restore_proof}, \bold{14} |
522 \item {\ptt rev_mp} theorem, \bold{92} |
525 \item {\tt result}, \bold{8}, 15, 55 |
523 \item rewrite rules, 96--97 |
526 \item {\tt rev_mp} theorem, \bold{97} |
524 \subitem permutative, 104--107 |
527 \item rewrite rules, 101--102 |
525 \item {\ptt rewrite_cterm}, \bold{44} |
528 \subitem permutative, 110--113 |
526 \item {\ptt rewrite_goals_rule}, \bold{36} |
529 \item {\tt rewrite_cterm}, \bold{47} |
527 \item {\ptt rewrite_goals_tac}, \bold{19}, 36 |
530 \item {\tt rewrite_goals_rule}, \bold{38} |
528 \item {\ptt rewrite_rule}, \bold{36} |
531 \item {\tt rewrite_goals_tac}, \bold{20}, 38 |
529 \item {\ptt rewrite_tac}, 8, \bold{19} |
532 \item {\tt rewrite_rule}, \bold{38} |
|
533 \item {\tt rewrite_tac}, 8, \bold{20} |
530 \item rewriting |
534 \item rewriting |
531 \subitem object-level, \see{simplification}{0} |
535 \subitem object-level, \see{simplification}{1} |
532 \subitem ordered, 104 |
536 \subitem ordered, 110 |
533 \subitem syntactic, 81--86 |
537 \subitem syntactic, 84--90 |
534 \item {\ptt rewtac}, \bold{18} |
538 \item {\tt rewtac}, \bold{19} |
535 \item {\ptt RL}, \bold{35} |
539 \item {\tt RL}, \bold{37} |
536 \item {\ptt RLN}, \bold{35} |
540 \item {\tt RLN}, \bold{37} |
537 \item {\ptt rotate_proof}, \bold{13} |
541 \item {\tt rotate_proof}, \bold{14} |
538 \item {\ptt rotate_tac}, \bold{20} |
542 \item {\tt rotate_tac}, \bold{22} |
539 \item {\ptt RS}, \bold{35} |
543 \item {\tt RS}, \bold{37} |
540 \item {\ptt RSN}, \bold{35} |
544 \item {\tt RSN}, \bold{37} |
541 \item {\ptt rtac}, \bold{17} |
545 \item {\tt rtac}, \bold{19} |
542 \item {\ptt rule_by_tactic}, 21, \bold{37} |
546 \item {\tt rule_by_tactic}, 22, \bold{39} |
543 \item rules |
547 \item rules |
544 \subitem converting destruction to elimination, 37 |
548 \subitem converting destruction to elimination, 39 |
545 |
549 |
546 \indexspace |
550 \indexspace |
547 |
551 |
548 \item {\ptt safe_asm_full_simp_tac}, \bold{98}, 100 |
552 \item {\tt safe_asm_full_simp_tac}, \bold{104}, 105 |
549 \item {\ptt safe_step_tac}, 117, \bold{120} |
553 \item {\tt safe_step_tac}, 123, \bold{126} |
550 \item {\ptt safe_tac}, \bold{120} |
554 \item {\tt safe_tac}, \bold{127} |
551 \item {\ptt save_proof}, \bold{13} |
555 \item {\tt save_proof}, \bold{14} |
552 \item saving your work, \bold{1} |
556 \item saving your work, \bold{1} |
553 \item search, 26 |
557 \item search, 28 |
554 \subitem tacticals, 28--30 |
558 \subitem tacticals, 30--32 |
555 \item {\ptt SELECT_GOAL}, 19, \bold{30} |
559 \item {\tt SELECT_GOAL}, 20, \bold{33} |
556 \item {\ptt Sequence.seq} ML type, 23 |
560 \item {\tt Sequence.seq} ML type, 25 |
557 \item sequences (lazy lists), \bold{24} |
561 \item sequences (lazy lists), \bold{26} |
558 \item sequent calculus, 112 |
562 \item sequent calculus, 118 |
559 \item sessions, 1--5 |
563 \item sessions, 1--5 |
560 \item {\ptt set_current_thy}, 96 |
564 \item {\tt set}, 3 |
561 \item {\ptt set_oracle}, \bold{60} |
565 \item {\tt set_current_thy}, 101 |
562 \item {\ptt setloop}, 99, 100 |
566 \item {\tt set_oracle}, \bold{61} |
563 \item {\ptt setmksimps}, 96, 100, 110 |
567 \item {\tt setloop}, 104, 105 |
564 \item {\ptt setSolver}, 98, 100, 110 |
568 \item {\tt setmksimps}, 102, 105, 116 |
565 \item {\ptt setSSolver}, 98, 100, 110 |
569 \item {\tt setSolver}, 104, 105, 116 |
566 \item {\ptt setsubgoaler}, 98, 100, 110 |
570 \item {\tt setSSolver}, 104, 105, 116 |
567 \item {\ptt setSWrapper}, \bold{118} |
571 \item {\tt setsubgoaler}, 103, 105, 116 |
568 \item {\ptt setWrapper}, \bold{118} |
572 \item {\tt setSWrapper}, \bold{124} |
569 \item shell scripts, \bold{4} |
573 \item {\tt setWrapper}, \bold{124} |
570 \item shortcuts |
574 \item shortcuts |
571 \subitem for tactics, 17 |
575 \subitem for tactics, 18 |
572 \subitem for {\tt by} commands, 10 |
576 \subitem for {\tt by} commands, 10 |
573 \item {\ptt show_brackets}, \bold{3} |
577 \item {\tt show_brackets}, \bold{4} |
574 \item {\ptt show_hyps}, \bold{3} |
578 \item {\tt show_hyps}, \bold{4} |
575 \item {\ptt show_sorts}, \bold{3}, 80 |
579 \item {\tt show_sorts}, \bold{4}, 83 |
576 \item {\ptt show_types}, \bold{3}, 80, 83, 89 |
580 \item {\tt show_types}, \bold{4}, 83, 86, 93 |
577 \item {\ptt Sign.cterm_of}, 7, 12 |
581 \item {\tt Sign.sg} ML type, 49 |
578 \item {\ptt Sign.sg} ML type, 46 |
582 \item {\tt Sign.string_of_term}, \bold{59} |
579 \item {\ptt Sign.string_of_term}, \bold{58} |
583 \item {\tt Sign.string_of_typ}, \bold{60} |
580 \item {\ptt Sign.string_of_typ}, \bold{59} |
584 \item {\tt sign_of}, 7, 13, \bold{56} |
581 \item {\ptt sign_of}, 7, 12, \bold{52} |
585 \item signatures, \bold{49}, 56, 58, 59, 61 |
582 \item signatures, \bold{46}, 53, 57--59 |
586 \item {\tt Simp_tac}, \bold{99}, 105 |
583 \item {\ptt Simp_tac}, \bold{94}, 100 |
587 \item {\tt simp_tac}, 105, \bold{106} |
584 \item {\ptt simp_tac}, \bold{99}, 100 |
588 \item simplification, 99--117 |
585 \item simplification, 94--111 |
589 \subitem from classical reasoner, 124 |
586 \subitem from classical reasoner, 117 |
590 \subitem setting up, 113 |
587 \subitem setting up, 107 |
591 \subitem tactics, 106 |
588 \subitem tactics, 99 |
592 \item simplification sets, 101 |
589 \item simplification sets, 96 |
|
590 \item simpset |
593 \item simpset |
591 \subitem current, 94, 96, 99 |
594 \subitem current, 99, 101, 106 |
592 \item {\ptt simpset}, 100 |
595 \item {\tt simpset}, 105 |
593 \item {\ptt simpset} ML type, 100 |
596 \item {\tt simpset} ML type, 105 |
594 \item {\tt simpset} ML value, 96 |
597 \item {\tt simpset} ML value, 101 |
595 \item {\ptt simpset_of}, 101 |
598 \item {\tt simpset_of}, 106 |
596 \item {\ptt size_of_thm}, 29, \bold{30}, 122 |
599 \item {\tt size_of_thm}, 31, \bold{32}, 129 |
597 \item {\ptt sizef}, \bold{122} |
600 \item {\tt sizef}, \bold{129} |
598 \item {\ptt slow_best_tac}, \bold{119} |
601 \item {\tt slow_best_tac}, \bold{126} |
599 \item {\ptt slow_step_tac}, 117, \bold{120} |
602 \item {\tt slow_step_tac}, 123, \bold{127} |
600 \item {\ptt slow_tac}, \bold{119} |
603 \item {\tt slow_tac}, \bold{126} |
601 \item {\ptt Some}, \bold{24} |
604 \item {\tt Some}, \bold{26} |
602 \item {\ptt SOMEGOAL}, \bold{32} |
605 \item {\tt SOMEGOAL}, \bold{34} |
603 \item {\ptt sort} nonterminal, \bold{65} |
606 \item {\tt sort} nonterminal, \bold{66} |
604 \item sort constraints, 64 |
607 \item sort constraints, 65 |
605 \item sort hypotheses, 37 |
608 \item sort hypotheses, 40 |
606 \item sorts |
609 \item sorts |
607 \subitem printing of, 3 |
610 \subitem printing of, 4 |
608 \item {\ptt split_tac}, \bold{111} |
611 \item {\tt split_tac}, \bold{116} |
609 \item {\ptt ssubst} theorem, \bold{90} |
612 \item {\tt ssubst} theorem, \bold{95} |
610 \item {\ptt stac}, \bold{91} |
613 \item {\tt stac}, \bold{96} |
611 \item stamps, 37, \bold{46}, 53 |
614 \item stamps, 39, \bold{49}, 56 |
612 \item {\ptt stamps_of_thm}, \bold{37} |
615 \item {\tt stamps_of_thm}, \bold{39} |
613 \item {\ptt stamps_of_thy}, \bold{53} |
616 \item {\tt stamps_of_thy}, \bold{56} |
614 \item {\ptt standard}, \bold{36} |
617 \item {\tt standard}, \bold{39} |
615 \item starting up, \bold{1} |
618 \item starting up, \bold{1} |
616 \item {\ptt STATE}, \bold{24} |
619 \item {\tt STATE}, \bold{25} |
617 \item {\ptt Step_tac}, \bold{121} |
620 \item {\tt Step_tac}, \bold{127} |
618 \item {\ptt step_tac}, 117, \bold{120} |
621 \item {\tt step_tac}, 123, \bold{127} |
619 \item {\ptt store_thm}, \bold{8} |
622 \item {\tt store_thm}, \bold{8} |
620 \item {\ptt string_of_cterm}, \bold{58} |
623 \item {\tt string_of_cterm}, \bold{59} |
621 \item {\ptt string_of_ctyp}, \bold{59} |
624 \item {\tt string_of_ctyp}, \bold{60} |
622 \item {\ptt string_of_thm}, \bold{35} |
625 \item {\tt string_of_thm}, \bold{37} |
623 \item strings, 65 |
626 \item strings, 66 |
624 \item {\ptt SUBGOAL}, \bold{24} |
627 \item {\tt SUBGOAL}, \bold{25} |
625 \item subgoal module, 6--14 |
628 \item subgoal module, 6--15 |
626 \item {\ptt subgoal_tac}, \bold{18} |
629 \item {\tt subgoal_tac}, \bold{19} |
627 \item {\ptt subgoals_of_brl}, \bold{22} |
630 \item {\tt subgoals_of_brl}, \bold{23} |
628 \item {\ptt subgoals_tac}, \bold{18} |
631 \item {\tt subgoals_tac}, \bold{19} |
629 \item {\ptt subst} theorem, 90, \bold{92} |
632 \item {\tt subst} theorem, 95, \bold{97} |
630 \item substitution |
633 \item substitution |
631 \subitem rules, 90 |
634 \subitem rules, 95 |
632 \item {\ptt swap} theorem, \bold{122} |
635 \item {\tt swap} theorem, \bold{129} |
633 \item {\ptt swap_res_tac}, \bold{121} |
636 \item {\tt swap_res_tac}, \bold{128} |
634 \item {\ptt swapify}, \bold{121} |
637 \item {\tt swapify}, \bold{128} |
635 \item {\ptt sym} theorem, 91, \bold{92} |
638 \item {\tt sym} theorem, 96, \bold{97} |
636 \item {\ptt symmetric}, \bold{41} |
639 \item {\tt symmetric}, \bold{43} |
637 \item {\ptt syn_of}, \bold{66} |
640 \item {\tt syn_of}, \bold{68} |
638 \item syntax |
641 \item syntax |
639 \subitem Pure, 63--68 |
642 \subitem Pure, 64--69 |
640 \subitem transformations, 76--89 |
643 \subitem transformations, 79--93 |
641 \item {\ptt syntax} section, 47 |
644 \item {\tt syntax} section, 50 |
642 \item {\ptt Syntax.ast} ML type, 76 |
645 \item {\tt Syntax.ast} ML type, 79 |
643 \item {\ptt Syntax.print_gram}, \bold{67} |
646 \item {\tt Syntax.mark_boundT}, 93 |
644 \item {\ptt Syntax.print_syntax}, \bold{66} |
647 \item {\tt Syntax.print_gram}, \bold{68} |
645 \item {\ptt Syntax.print_trans}, \bold{67} |
648 \item {\tt Syntax.print_syntax}, \bold{68} |
646 \item {\ptt Syntax.stat_norm_ast}, 84 |
649 \item {\tt Syntax.print_trans}, \bold{68} |
647 \item {\ptt Syntax.syntax} ML type, 66 |
650 \item {\tt Syntax.stat_norm_ast}, 88 |
648 \item {\ptt Syntax.test_read}, 70, 84 |
651 \item {\tt Syntax.syntax} ML type, 68 |
649 \item {\ptt Syntax.trace_norm_ast}, 84 |
652 \item {\tt Syntax.test_read}, 72, 88 |
650 |
653 \item {\tt Syntax.trace_norm_ast}, 88 |
651 \indexspace |
654 \item {\tt Syntax.variant_abs'}, 93 |
652 |
655 |
653 \item {\ptt Tactic}, \bold{24} |
656 \indexspace |
654 \item {\ptt tactic} ML type, 15 |
657 |
655 \item tacticals, 26--33 |
658 \item {\tt tactic} ML type, 16 |
656 \subitem conditional, 29 |
659 \item tacticals, 28--35 |
657 \subitem deterministic, 29 |
660 \subitem conditional, 32 |
658 \subitem for filtering, 28 |
661 \subitem deterministic, 32 |
659 \subitem for restriction to a subgoal, 30 |
662 \subitem for filtering, 30 |
660 \subitem identities for, 27 |
663 \subitem for restriction to a subgoal, 33 |
661 \subitem joining a list of tactics, 26 |
664 \subitem identities for, 29 |
662 \subitem joining tactic functions, 32, 33 |
665 \subitem joining a list of tactics, 29 |
663 \subitem joining two tactics, 26 |
666 \subitem joining tactic functions, 35 |
664 \subitem repetition, 27 |
667 \subitem joining two tactics, 28 |
665 \subitem scanning for subgoals, 31 |
668 \subitem repetition, 29 |
666 \subitem searching, 28, 29 |
669 \subitem scanning for subgoals, 34 |
667 \item tactics, 15--25 |
670 \subitem searching, 31 |
668 \subitem assumption, \bold{16}, 17 |
671 \item tactics, 16--27 |
|
672 \subitem assumption, \bold{17}, 18 |
669 \subitem commands for applying, 7 |
673 \subitem commands for applying, 7 |
670 \subitem debugging, 13 |
674 \subitem debugging, 14 |
671 \subitem filtering results of, 28 |
675 \subitem filtering results of, 30 |
672 \subitem for composition, 21 |
676 \subitem for composition, 22 |
673 \subitem for contradiction, 121 |
677 \subitem for contradiction, 128 |
674 \subitem for inserting facts, 18 |
678 \subitem for inserting facts, 19 |
675 \subitem for Modus Ponens, 121 |
679 \subitem for Modus Ponens, 128 |
676 \subitem instantiation, 16 |
680 \subitem instantiation, 17 |
677 \subitem matching, 16 |
681 \subitem matching, 17 |
678 \subitem meta-rewriting, 17, \bold{18} |
682 \subitem meta-rewriting, 18, \bold{20} |
679 \subitem primitives for coding, 23 |
683 \subitem primitives for coding, 25 |
680 \subitem resolution, \bold{15}, 17, 21, 22 |
684 \subitem resolution, \bold{16}, 18, 23, 24 |
681 \subitem restricting to a subgoal, 30 |
685 \subitem restricting to a subgoal, 33 |
682 \subitem simplification, 99 |
686 \subitem simplification, 106 |
683 \subitem substitution, 90--93 |
687 \subitem substitution, 95--98 |
684 \subitem tracing, 24 |
688 \subitem tracing, 25 |
685 \item {\ptt tapply}, \bold{23} |
689 \item {\tt TERM}, 59 |
686 \item {\ptt teeinput} shell script, 5 |
690 \item {\tt term} ML type, 57, 82 |
687 \item {\ptt TERM}, 58 |
691 \item terms, \bold{57} |
688 \item {\ptt term} ML type, 56, 79 |
692 \subitem certified, \bold{58} |
689 \item terms, \bold{56} |
693 \subitem made from ASTs, 82 |
690 \subitem certified, \bold{57} |
694 \subitem printing of, 14, 59 |
691 \subitem made from ASTs, 79 |
|
692 \subitem printing of, 14, 58 |
|
693 \subitem reading of, 14 |
695 \subitem reading of, 14 |
694 \item {\ptt TFree}, \bold{59} |
696 \item {\tt TFree}, \bold{60} |
695 \item {\ptt THEN}, \bold{26}, 27, 32 |
697 \item {\tt THEN}, \bold{28}, 30, 34 |
696 \item {\ptt THEN'}, 33 |
698 \item {\tt THEN'}, 35 |
697 \item {\ptt THEN_BEST_FIRST}, \bold{29} |
699 \item {\tt THEN_BEST_FIRST}, \bold{31} |
698 \item theorems, 34--45 |
700 \item theorems, 36--48 |
699 \subitem equality of, 30 |
701 \subitem equality of, 32 |
700 \subitem extracting, 51 |
702 \subitem extracting, 55 |
701 \subitem extracting proved, 8 |
703 \subitem extracting proved, 8 |
702 \subitem joining by resolution, 35 |
704 \subitem joining by resolution, 37 |
703 \subitem of pure theory, 19 |
705 \subitem of pure theory, 20 |
704 \subitem printing of, 34 |
706 \subitem printing of, 36 |
705 \subitem retrieving, 8 |
707 \subitem retrieving, 9 |
706 \subitem size of, 30 |
708 \subitem size of, 32 |
707 \subitem standardizing, 36 |
709 \subitem standardizing, 38 |
708 \subitem storing, 8 |
710 \subitem storing, 8 |
709 \subitem taking apart, 37 |
711 \subitem taking apart, 39 |
710 \item theories, 46--61 |
712 \item theories, 49--62 |
711 \subitem axioms of, 51 |
713 \subitem axioms of, 55 |
712 \subitem constructing, \bold{52} |
714 \subitem constructing, \bold{55} |
713 \subitem inspecting, \bold{52} |
715 \subitem inspecting, \bold{56} |
714 \subitem loading, 49 |
716 \subitem loading, 52 |
715 \subitem parent, \bold{46} |
717 \subitem parent, \bold{49} |
716 \subitem pseudo, \bold{50} |
718 \subitem pseudo, \bold{54} |
717 \subitem reloading, \bold{50} |
719 \subitem reloading, \bold{53} |
718 \subitem removing, \bold{50} |
720 \subitem removing, \bold{54} |
719 \subitem theorems of, 51 |
721 \subitem theorems of, 55 |
720 \item {\ptt THEORY} exception, 46, 51 |
722 \item {\tt THEORY} exception, 49, 55 |
721 \item {\ptt theory} ML type, 46 |
723 \item {\tt theory} ML type, 49 |
722 \item {\ptt theory_of_thm}, \bold{37} |
724 \item {\tt theory_of_thm}, \bold{39} |
723 \item {\ptt thin_tac}, \bold{20} |
725 \item {\tt thin_tac}, \bold{22} |
724 \item {\ptt THM} exception, 34, 35, 39, 43 |
726 \item {\tt THM} exception, 36, 37, 41, 46 |
725 \item {\ptt thm} ML type, 34 |
727 \item {\tt thm} ML type, 36 |
726 \item {\ptt thms_containing}, \bold{9} |
728 \item {\tt thms_containing}, \bold{9} |
727 \item {\ptt thms_of}, \bold{52} |
729 \item {\tt thms_of}, \bold{56} |
728 \item {\ptt tid} nonterminal, \bold{65}, 77, 84 |
730 \item {\tt tid} nonterminal, \bold{66}, 80, 87 |
729 \item {\ptt time_use}, \bold{2} |
731 \item {\tt time_use}, \bold{3} |
730 \item {\ptt time_use_thy}, \bold{49} |
732 \item {\tt time_use_thy}, \bold{53} |
731 \item timing statistics, 10 |
733 \item timing statistics, 10 |
732 \item {\ptt topthm}, \bold{14} |
734 \item {\tt toggle}, 3 |
733 \item {\ptt tpairs_of}, \bold{37} |
735 \item token class, 93 |
734 \item {\ptt trace_BEST_FIRST}, \bold{29} |
736 \item token translations, 93--94 |
735 \item {\ptt trace_DEPTH_FIRST}, \bold{29} |
737 \item token_translation, 94 |
736 \item {\ptt trace_goalno_tac}, \bold{32} |
738 \item {\tt token_translation}, 94 |
737 \item {\ptt trace_REPEAT}, \bold{27} |
739 \item {\tt topthm}, \bold{15} |
738 \item {\ptt trace_simp}, 95, 102--103 |
740 \item {\tt tpairs_of}, \bold{39} |
|
741 \item {\tt trace_BEST_FIRST}, \bold{31} |
|
742 \item {\tt trace_DEPTH_FIRST}, \bold{31} |
|
743 \item {\tt trace_goalno_tac}, \bold{34} |
|
744 \item {\tt trace_REPEAT}, \bold{29} |
|
745 \item {\tt trace_simp}, 100, 108 |
739 \item tracing |
746 \item tracing |
740 \subitem of classical prover, 119 |
747 \subitem of classical prover, 125 |
741 \subitem of macros, 84 |
748 \subitem of macros, 88 |
742 \subitem of searching tacticals, 28, 29 |
749 \subitem of searching tacticals, 31 |
743 \subitem of simplification, 95, 102--103 |
750 \subitem of simplification, 100, 108--109 |
744 \subitem of tactics, 24 |
751 \subitem of tactics, 25 |
745 \subitem of unification, 38 |
752 \subitem of unification, 40 |
746 \item {\ptt transitive}, \bold{41} |
753 \item {\tt transitive}, \bold{43} |
747 \item translations, 86--89 |
754 \item translations, 90--93 |
748 \subitem parse, 72, 79 |
755 \subitem parse, 74, 82 |
749 \subitem parse AST, \bold{77}, 78 |
756 \subitem parse AST, \bold{80}, 81 |
750 \subitem print, 72 |
757 \subitem print, 74 |
751 \subitem print AST, \bold{80} |
758 \subitem print AST, \bold{83} |
752 \item {\ptt translations} section, 82 |
759 \item {\tt translations} section, 85 |
753 \item {\ptt trivial}, \bold{44} |
760 \item {\tt trivial}, \bold{46} |
754 \item {\ptt Trueprop} constant, 73 |
761 \item {\tt Trueprop} constant, 76 |
755 \item {\ptt TRY}, \bold{27, 28} |
762 \item {\tt TRY}, \bold{29, 30} |
756 \item {\ptt TRYALL}, \bold{32} |
763 \item {\tt TRYALL}, \bold{34} |
757 \item {\ptt TVar}, \bold{59} |
764 \item {\tt TVar}, \bold{60} |
758 \item {\ptt tvar} nonterminal, \bold{65, 66}, 77, 84 |
765 \item {\tt tvar} nonterminal, \bold{66, 67}, 80, 87 |
759 \item {\ptt typ} ML type, 58 |
766 \item {\tt typ} ML type, 60 |
760 \item {\ptt Type}, \bold{59} |
767 \item {\tt Type}, \bold{60} |
761 \item {\ptt type} nonterminal, \bold{65} |
768 \item {\tt type} nonterminal, \bold{66} |
762 \item {\ptt type} type, 69 |
769 \item {\tt type} type, 71 |
763 \item type constraints, 65, 72, 80 |
770 \item type constraints, 66, 74, 83 |
764 \item type constructors, \bold{59} |
771 \item type constructors, \bold{60} |
765 \item type identifiers, 65 |
772 \item type identifiers, 66 |
766 \item type synonyms, \bold{47} |
773 \item type synonyms, \bold{50} |
767 \item type unknowns, \bold{59}, 65 |
774 \item type unknowns, \bold{60}, 66 |
768 \subitem freezing/thawing of, 42 |
775 \subitem freezing/thawing of, 45 |
769 \item type variables, \bold{59} |
776 \item type variables, \bold{60} |
770 \item types, \bold{58} |
777 \item types, \bold{60} |
771 \subitem certified, \bold{59} |
778 \subitem certified, \bold{60} |
772 \subitem printing of, 3, 14, 59 |
779 \subitem printing of, 4, 14, 60 |
773 |
780 |
774 \indexspace |
781 \indexspace |
775 |
782 |
776 \item {\ptt undo}, 6, \bold{9}, 13 |
783 \item {\tt undo}, 6, \bold{9}, 13 |
777 \item unknowns, \bold{56}, 65 |
784 \item unknowns, \bold{57}, 66 |
778 \item {\ptt unlink_thy}, \bold{50} |
785 \item {\tt unlink_thy}, \bold{54} |
779 \item {\ptt update}, \bold{50} |
786 \item {\tt update}, \bold{54} |
780 \item {\ptt uresult}, \bold{8}, 14, 52 |
787 \item {\tt uresult}, \bold{8}, 15, 55 |
781 \item {\ptt use}, \bold{2} |
788 \item {\tt use}, \bold{3} |
782 \item use_dir, 54, 55 |
789 \item {\tt use_thy}, \bold{52}, 53 |
783 \item {\ptt use_thy}, \bold{49}, 50 |
790 |
784 |
791 \indexspace |
785 \indexspace |
792 |
786 |
793 \item {\tt Var}, \bold{57}, 82 |
787 \item {\ptt Var}, \bold{56}, 79 |
794 \item {\tt var} nonterminal, \bold{66, 67}, 80, 87 |
788 \item {\ptt var} nonterminal, \bold{65, 66}, 77, 84 |
795 \item {\tt Variable}, 79 |
789 \item {\ptt Variable}, 76 |
|
790 \item variables |
796 \item variables |
791 \subitem bound, \bold{56} |
797 \subitem bound, \bold{57} |
792 \subitem free, \bold{56} |
798 \subitem free, \bold{57} |
793 \item {\ptt variant_abs}, \bold{57}, 89 |
799 \item {\tt variant_abs}, \bold{58} |
794 \item {\ptt varifyT}, \bold{42} |
800 \item {\tt varifyT}, \bold{45} |
795 |
801 |
796 \indexspace |
802 \indexspace |
797 |
803 |
798 \item {\ptt xlisten} shell script, 5 |
804 \item {\tt xnum} nonterminal, \bold{66}, 80, 87 |
799 \item {\ptt xnum} nonterminal, \bold{65}, 77, 84 |
805 \item {\tt xstr} nonterminal, \bold{66}, 80, 87 |
800 \item {\ptt xstr} nonterminal, \bold{65}, 77, 84 |
806 |
801 |
807 \indexspace |
802 \indexspace |
808 |
803 |
809 \item {\tt zero_var_indexes}, \bold{39} |
804 \item {\ptt zero_var_indexes}, \bold{36} |
|
805 |
810 |
806 \end{theindex} |
811 \end{theindex} |