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