1 \begin{theindex} |
|
2 |
|
3 \item {\tt\#*} symbol, 30 |
|
4 \item {\tt\#+} symbol, 30 |
|
5 \item {\tt\&} symbol, 6 |
|
6 \item {\tt *} symbol, 21 |
|
7 \item {\tt +} symbol, 21 |
|
8 \item {\tt -} symbol, 30 |
|
9 \item {\tt -->} symbol, 6, 21 |
|
10 \item {\tt <->} symbol, 6 |
|
11 \item {\tt =} symbol, 6, 21 |
|
12 \item {\tt `} symbol, 21 |
|
13 \item {\tt |} symbol, 6 |
|
14 \item {\tt |-|} symbol, 30 |
|
15 |
|
16 \indexspace |
|
17 |
|
18 \item {\tt 0} constant, 19 |
|
19 |
|
20 \indexspace |
|
21 |
|
22 \item {\tt absdiff_def} theorem, 30 |
|
23 \item {\tt add_assoc} theorem, 30 |
|
24 \item {\tt add_commute} theorem, 30 |
|
25 \item {\tt add_def} theorem, 30 |
|
26 \item {\tt add_inverse_diff} theorem, 30 |
|
27 \item {\tt add_mp_tac}, \bold{28} |
|
28 \item {\tt add_mult_dist} theorem, 30 |
|
29 \item {\tt add_safes}, \bold{12} |
|
30 \item {\tt add_typing} theorem, 30 |
|
31 \item {\tt add_unsafes}, \bold{12} |
|
32 \item {\tt addC0} theorem, 30 |
|
33 \item {\tt addC_succ} theorem, 30 |
|
34 \item {\tt ALL} symbol, 6 |
|
35 \item {\tt All} constant, 6 |
|
36 \item {\tt allL} theorem, 8, 12 |
|
37 \item {\tt allL_thin} theorem, 9 |
|
38 \item {\tt allR} theorem, 8 |
|
39 \item {\tt Arith} theory, 29 |
|
40 \item assumptions |
|
41 \subitem in {\CTT}, 18, 28 |
|
42 |
|
43 \indexspace |
|
44 |
|
45 \item {\tt basic} theorem, 8 |
|
46 \item {\tt basic_defs}, \bold{26} |
|
47 \item {\tt best_tac}, \bold{13} |
|
48 |
|
49 \indexspace |
|
50 |
|
51 \item {\tt CCL} theory, 1 |
|
52 \item {\tt comp_rls}, \bold{26} |
|
53 \item {\tt conjL} theorem, 8 |
|
54 \item {\tt conjR} theorem, 8 |
|
55 \item {\tt conL} theorem, 9 |
|
56 \item {\tt conR} theorem, 9 |
|
57 \item Constructive Type Theory, 18--40 |
|
58 \item {\tt contr} constant, 19 |
|
59 \item {\tt could_res}, \bold{11} |
|
60 \item {\tt could_resolve_seq}, \bold{11} |
|
61 \item {\tt CTT} theory, 1, 18 |
|
62 \item {\tt Cube} theory, 1 |
|
63 \item {\tt cut} theorem, 8 |
|
64 \item {\tt cutL_tac}, \bold{10} |
|
65 \item {\tt cutR_tac}, \bold{10} |
|
66 |
|
67 \indexspace |
|
68 |
|
69 \item {\tt diff_0_eq_0} theorem, 30 |
|
70 \item {\tt diff_def} theorem, 30 |
|
71 \item {\tt diff_self_eq_0} theorem, 30 |
|
72 \item {\tt diff_succ_succ} theorem, 30 |
|
73 \item {\tt diff_typing} theorem, 30 |
|
74 \item {\tt diffC0} theorem, 30 |
|
75 \item {\tt disjL} theorem, 8 |
|
76 \item {\tt disjR} theorem, 8 |
|
77 \item {\tt div} symbol, 30 |
|
78 \item {\tt div_def} theorem, 30 |
|
79 |
|
80 \indexspace |
|
81 |
|
82 \item {\tt Elem} constant, 19 |
|
83 \item {\tt elim_rls}, \bold{26} |
|
84 \item {\tt elimL_rls}, \bold{26} |
|
85 \item {\tt empty_pack}, \bold{12} |
|
86 \item {\tt Eq} constant, 19 |
|
87 \item {\tt eq} constant, 19, 24 |
|
88 \item {\tt EqC} theorem, 25 |
|
89 \item {\tt EqE} theorem, 25 |
|
90 \item {\tt Eqelem} constant, 19 |
|
91 \item {\tt EqF} theorem, 25 |
|
92 \item {\tt EqFL} theorem, 25 |
|
93 \item {\tt EqI} theorem, 25 |
|
94 \item {\tt Eqtype} constant, 19 |
|
95 \item {\tt equal_tac}, \bold{27} |
|
96 \item {\tt equal_types} theorem, 22 |
|
97 \item {\tt equal_typesL} theorem, 22 |
|
98 \item {\tt EX} symbol, 6 |
|
99 \item {\tt Ex} constant, 6 |
|
100 \item {\tt exL} theorem, 8 |
|
101 \item {\tt exR} theorem, 8, 12, 14 |
|
102 \item {\tt exR_thin} theorem, 9, 14, 15 |
|
103 |
|
104 \indexspace |
|
105 |
|
106 \item {\tt F} constant, 19 |
|
107 \item {\tt False} constant, 6 |
|
108 \item {\tt FalseL} theorem, 8 |
|
109 \item {\tt fast_tac}, \bold{13} |
|
110 \item {\tt FE} theorem, 25, 29 |
|
111 \item {\tt FEL} theorem, 25 |
|
112 \item {\tt FF} theorem, 25 |
|
113 \item {\tt filseq_resolve_tac}, \bold{11} |
|
114 \item {\tt filt_resolve_tac}, 11, 27 |
|
115 \item flex-flex constraints, 7 |
|
116 \item {\tt FOL} theory, 28 |
|
117 \item {\tt form_rls}, \bold{26} |
|
118 \item {\tt formL_rls}, \bold{26} |
|
119 \item {\tt forms_of_seq}, \bold{10} |
|
120 \item {\tt fst} constant, 19, 24 |
|
121 \item {\tt fst_def} theorem, 24 |
|
122 \item function applications |
|
123 \subitem in \CTT, 21 |
|
124 |
|
125 \indexspace |
|
126 |
|
127 \item {\tt HOL} theory, 1 |
|
128 \item {\tt HOLCF} theory, 1 |
|
129 \item {\tt hyp_rew_tac}, \bold{28} |
|
130 |
|
131 \indexspace |
|
132 |
|
133 \item {\textit {i}} type, 18 |
|
134 \item {\tt iff_def} theorem, 8 |
|
135 \item {\tt iffL} theorem, 9, 16 |
|
136 \item {\tt iffR} theorem, 9 |
|
137 \item {\tt ILL} theory, 1 |
|
138 \item {\tt impL} theorem, 8 |
|
139 \item {\tt impR} theorem, 8 |
|
140 \item {\tt inl} constant, 19, 24, 34 |
|
141 \item {\tt inr} constant, 19, 24 |
|
142 \item {\tt intr_rls}, \bold{26} |
|
143 \item {\tt intr_tac}, \bold{27}, 36, 37 |
|
144 \item {\tt intrL_rls}, \bold{26} |
|
145 |
|
146 \indexspace |
|
147 |
|
148 \item {\tt lam} symbol, 21 |
|
149 \item {\tt lambda} constant, 19, 21 |
|
150 \item $\lambda$-abstractions |
|
151 \subitem in \CTT, 21 |
|
152 \item {\tt LCF} theory, 1 |
|
153 \item {\tt LK} theory, 1, 5, 9 |
|
154 \item {\tt LK_dup_pack}, \bold{12}, 13 |
|
155 \item {\tt LK_pack}, \bold{12} |
|
156 |
|
157 \indexspace |
|
158 |
|
159 \item {\tt mod} symbol, 30 |
|
160 \item {\tt mod_def} theorem, 30 |
|
161 \item {\tt Modal} theory, 1 |
|
162 \item {\tt mp_tac}, \bold{28} |
|
163 \item {\tt mult_assoc} theorem, 30 |
|
164 \item {\tt mult_commute} theorem, 30 |
|
165 \item {\tt mult_def} theorem, 30 |
|
166 \item {\tt mult_typing} theorem, 30 |
|
167 \item {\tt multC0} theorem, 30 |
|
168 \item {\tt multC_succ} theorem, 30 |
|
169 |
|
170 \indexspace |
|
171 |
|
172 \item {\tt N} constant, 19 |
|
173 \item {\tt NC0} theorem, 23 |
|
174 \item {\tt NC_succ} theorem, 23 |
|
175 \item {\tt NE} theorem, 22, 23, 31 |
|
176 \item {\tt NEL} theorem, 23 |
|
177 \item {\tt NF} theorem, 23, 32 |
|
178 \item {\tt NI0} theorem, 23 |
|
179 \item {\tt NI_succ} theorem, 23 |
|
180 \item {\tt NI_succL} theorem, 23 |
|
181 \item {\tt NIO} theorem, 31 |
|
182 \item {\tt Not} constant, 6 |
|
183 \item {\tt notL} theorem, 8 |
|
184 \item {\tt notR} theorem, 8 |
|
185 |
|
186 \indexspace |
|
187 |
|
188 \item {\textit {o}} type, 5 |
|
189 |
|
190 \indexspace |
|
191 |
|
192 \item {\tt pack} ML type, 11 |
|
193 \item {\tt pair} constant, 19 |
|
194 \item {\tt pc_tac}, \bold{13}, \bold{29}, 35, 36 |
|
195 \item {\tt PlusC_inl} theorem, 25 |
|
196 \item {\tt PlusC_inr} theorem, 25 |
|
197 \item {\tt PlusE} theorem, 25, 29, 33 |
|
198 \item {\tt PlusEL} theorem, 25 |
|
199 \item {\tt PlusF} theorem, 25 |
|
200 \item {\tt PlusFL} theorem, 25 |
|
201 \item {\tt PlusI_inl} theorem, 25, 34 |
|
202 \item {\tt PlusI_inlL} theorem, 25 |
|
203 \item {\tt PlusI_inr} theorem, 25 |
|
204 \item {\tt PlusI_inrL} theorem, 25 |
|
205 \item priorities, 3 |
|
206 \item {\tt PROD} symbol, 20, 21 |
|
207 \item {\tt Prod} constant, 19 |
|
208 \item {\tt ProdC} theorem, 23, 39 |
|
209 \item {\tt ProdC2} theorem, 23 |
|
210 \item {\tt ProdE} theorem, 23, 36, 38, 40 |
|
211 \item {\tt ProdEL} theorem, 23 |
|
212 \item {\tt ProdF} theorem, 23 |
|
213 \item {\tt ProdFL} theorem, 23 |
|
214 \item {\tt ProdI} theorem, 23, 29, 31 |
|
215 \item {\tt ProdIL} theorem, 23 |
|
216 \item {\tt prop_pack}, \bold{12} |
|
217 |
|
218 \indexspace |
|
219 |
|
220 \item {\tt rec} constant, 19, 22 |
|
221 \item {\tt red_if_equal} theorem, 22 |
|
222 \item {\tt Reduce} constant, 19, 22, 28 |
|
223 \item {\tt refl} theorem, 8 |
|
224 \item {\tt refl_elem} theorem, 22, 26 |
|
225 \item {\tt refl_red} theorem, 22 |
|
226 \item {\tt refl_type} theorem, 22, 26 |
|
227 \item {\tt REPEAT_FIRST}, 27 |
|
228 \item {\tt repeat_goal_tac}, \bold{13} |
|
229 \item {\tt replace_type} theorem, 26, 38 |
|
230 \item {\tt reresolve_tac}, \bold{13} |
|
231 \item {\tt rew_tac}, \bold{28} |
|
232 \item {\tt RL}, 33 |
|
233 \item {\tt RS}, 38, 40 |
|
234 |
|
235 \indexspace |
|
236 |
|
237 \item {\tt safe_goal_tac}, \bold{13} |
|
238 \item {\tt safe_tac}, \bold{29} |
|
239 \item {\tt safestep_tac}, \bold{29} |
|
240 \item {\tt Seqof} constant, 6 |
|
241 \item sequent calculus, 5--17 |
|
242 \item {\tt snd} constant, 19, 24 |
|
243 \item {\tt snd_def} theorem, 24 |
|
244 \item {\tt sobj} type, 9 |
|
245 \item {\tt split} constant, 19, 33 |
|
246 \item {\tt step_tac}, \bold{13}, \bold{29} |
|
247 \item {\tt subst_elem} theorem, 22 |
|
248 \item {\tt subst_elemL} theorem, 22 |
|
249 \item {\tt subst_eqtyparg} theorem, 26, 38 |
|
250 \item {\tt subst_prodE} theorem, 24, 26 |
|
251 \item {\tt subst_type} theorem, 22 |
|
252 \item {\tt subst_typeL} theorem, 22 |
|
253 \item {\tt succ} constant, 19 |
|
254 \item {\tt SUM} symbol, 20, 21 |
|
255 \item {\tt Sum} constant, 19 |
|
256 \item {\tt SumC} theorem, 24 |
|
257 \item {\tt SumE} theorem, 24, 29, 33 |
|
258 \item {\tt SumE_fst} theorem, 24, 26, 38, 39 |
|
259 \item {\tt SumE_snd} theorem, 24, 26, 40 |
|
260 \item {\tt SumEL} theorem, 24 |
|
261 \item {\tt SumF} theorem, 24 |
|
262 \item {\tt SumFL} theorem, 24 |
|
263 \item {\tt SumI} theorem, 24, 34 |
|
264 \item {\tt SumIL} theorem, 24 |
|
265 \item {\tt SumIL2} theorem, 26 |
|
266 \item {\tt sym} theorem, 8 |
|
267 \item {\tt sym_elem} theorem, 22 |
|
268 \item {\tt sym_type} theorem, 22 |
|
269 \item {\tt symL} theorem, 9 |
|
270 |
|
271 \indexspace |
|
272 |
|
273 \item {\tt T} constant, 19 |
|
274 \item {\textit {t}} type, 18 |
|
275 \item {\tt TC} theorem, 25 |
|
276 \item {\tt TE} theorem, 25 |
|
277 \item {\tt TEL} theorem, 25 |
|
278 \item {\tt term} class, 5 |
|
279 \item {\tt test_assume_tac}, \bold{27} |
|
280 \item {\tt TF} theorem, 25 |
|
281 \item {\tt THE} symbol, 6 |
|
282 \item {\tt The} constant, 6 |
|
283 \item {\tt The} theorem, 8 |
|
284 \item {\tt thinL} theorem, 8 |
|
285 \item {\tt thinR} theorem, 8 |
|
286 \item {\tt TI} theorem, 25 |
|
287 \item {\tt trans} theorem, 8 |
|
288 \item {\tt trans_elem} theorem, 22 |
|
289 \item {\tt trans_red} theorem, 22 |
|
290 \item {\tt trans_type} theorem, 22 |
|
291 \item {\tt True} constant, 6 |
|
292 \item {\tt True_def} theorem, 8 |
|
293 \item {\tt Trueprop} constant, 6 |
|
294 \item {\tt TrueR} theorem, 9 |
|
295 \item {\tt tt} constant, 19 |
|
296 \item {\tt Type} constant, 19 |
|
297 \item {\tt typechk_tac}, \bold{27}, 32, 35, 39, 40 |
|
298 |
|
299 \indexspace |
|
300 |
|
301 \item {\tt when} constant, 19, 24, 33 |
|
302 |
|
303 \indexspace |
|
304 |
|
305 \item {\tt zero_ne_succ} theorem, 22, 23 |
|
306 |
|
307 \end{theindex} |
|