105
|
1 |
\begin{theindex}
|
|
2 |
|
2664
|
3 |
\item {\ptt !!} symbol, 25
|
|
4 |
\subitem in main goal, 46
|
|
5 |
\item {\tt\%} symbol, 25
|
|
6 |
\item {\ptt ::} symbol, 25
|
|
7 |
\item {\ptt ==} symbol, 25
|
|
8 |
\item {\ptt ==>} symbol, 25
|
|
9 |
\item {\ptt =>} symbol, 25
|
|
10 |
\item {\ptt =?=} symbol, 25
|
|
11 |
\item {\ptt [} symbol, 25
|
|
12 |
\item {\ptt [|} symbol, 25
|
|
13 |
\item {\ptt ]} symbol, 25
|
|
14 |
\item {\tt\ttlbrace} symbol, 25
|
|
15 |
\item {\tt\ttrbrace} symbol, 25
|
|
16 |
\item {\ptt |]} symbol, 25
|
105
|
17 |
|
|
18 |
\indexspace
|
|
19 |
|
2664
|
20 |
\item {\ptt allI} theorem, 37
|
359
|
21 |
\item arities
|
2664
|
22 |
\subitem declaring, 4, \bold{49}
|
|
23 |
\item {\ptt asm_simp_tac}, 60
|
|
24 |
\item {\ptt assume_tac}, 29, 31, 37, 47
|
359
|
25 |
\item assumptions
|
2664
|
26 |
\subitem deleting, 20
|
359
|
27 |
\subitem discharge of, 7
|
2664
|
28 |
\subitem lifting over, 14
|
|
29 |
\subitem of main goal, 41
|
|
30 |
\subitem use of, 16, 28
|
359
|
31 |
\item axioms
|
2664
|
32 |
\subitem Peano, 54
|
105
|
33 |
|
|
34 |
\indexspace
|
|
35 |
|
2664
|
36 |
\item {\ptt ba}, 30
|
|
37 |
\item {\ptt back}, 59, 62
|
359
|
38 |
\item backtracking
|
2664
|
39 |
\subitem Prolog style, 62
|
|
40 |
\item {\ptt bd}, 30
|
|
41 |
\item {\ptt be}, 30
|
|
42 |
\item {\ptt br}, 30
|
|
43 |
\item {\ptt by}, 30
|
105
|
44 |
|
|
45 |
\indexspace
|
|
46 |
|
2664
|
47 |
\item {\ptt choplev}, 36, 37, 64
|
359
|
48 |
\item classes, 3
|
2664
|
49 |
\subitem built-in, \bold{25}
|
|
50 |
\item classical reasoner, 39
|
|
51 |
\item {\ptt conjunct1} theorem, 27
|
359
|
52 |
\item constants, 1
|
|
53 |
\subitem clashes with variables, 9
|
2664
|
54 |
\subitem declaring, \bold{48}
|
|
55 |
\subitem overloaded, 53
|
359
|
56 |
\subitem polymorphic, 3
|
|
57 |
|
|
58 |
\indexspace
|
|
59 |
|
2664
|
60 |
\item definitions, 6, \bold{48}
|
|
61 |
\subitem and derived rules, 43--46
|
|
62 |
\item {\ptt DEPTH_FIRST}, 64
|
|
63 |
\item destruct-resolution, 22, 30
|
|
64 |
\item {\ptt disjE} theorem, 31
|
|
65 |
\item {\ptt dres_inst_tac}, 57
|
|
66 |
\item {\ptt dresolve_tac}, 30, 32, 38
|
105
|
67 |
|
|
68 |
\indexspace
|
|
69 |
|
2664
|
70 |
\item eigenvariables, \see{parameters}{8}
|
|
71 |
\item elim-resolution, \bold{20}, 30
|
105
|
72 |
\item equality
|
359
|
73 |
\subitem polymorphic, 3
|
2664
|
74 |
\item {\ptt eres_inst_tac}, 57
|
|
75 |
\item {\ptt eresolve_tac}, 30, 32, 38, 47
|
105
|
76 |
\item examples
|
2664
|
77 |
\subitem of deriving rules, 41
|
|
78 |
\subitem of induction, 57, 58
|
|
79 |
\subitem of simplification, 59
|
|
80 |
\subitem of tacticals, 37
|
|
81 |
\subitem of theories, 48, 50--55, 61
|
|
82 |
\subitem propositional, 17, 31, 32
|
|
83 |
\subitem with quantifiers, 18, 33, 35, 37
|
|
84 |
\item {\ptt exE} theorem, 38
|
105
|
85 |
|
|
86 |
\indexspace
|
|
87 |
|
2664
|
88 |
\item {\ptt FalseE} theorem, 45
|
|
89 |
\item {\ptt fast_tac}, 39
|
359
|
90 |
\item first-order logic, 1
|
2664
|
91 |
\item flex-flex constraints, 6, 25, \bold{28}
|
|
92 |
\item {\ptt flexflex_rule}, 28
|
|
93 |
\item forward proof, 21, 24--30
|
359
|
94 |
\item {\ptt fun} type, 1, 4
|
2664
|
95 |
\item function applications, 1, 8
|
105
|
96 |
|
|
97 |
\indexspace
|
|
98 |
|
2664
|
99 |
\item {\ptt goal}, 30, 41, 46
|
|
100 |
\item {\ptt goalw}, 44--46
|
359
|
101 |
|
|
102 |
\indexspace
|
|
103 |
|
2664
|
104 |
\item {\ptt has_fewer_prems}, 64
|
359
|
105 |
\item higher-order logic, 4
|
105
|
106 |
|
|
107 |
\indexspace
|
|
108 |
|
2664
|
109 |
\item identifiers, 24
|
|
110 |
\item {\ptt impI} theorem, 31, 44
|
|
111 |
\item infixes, 52
|
|
112 |
\item instantiation, 57--60
|
105
|
113 |
\item Isabelle
|
|
114 |
\subitem object-logics supported, i
|
|
115 |
\subitem overview, i
|
|
116 |
\subitem release history, i
|
|
117 |
|
|
118 |
\indexspace
|
|
119 |
|
2664
|
120 |
\item $\lambda$-abstractions, 1, 8, 25
|
359
|
121 |
\item $\lambda$-calculus, 1
|
|
122 |
\item LCF, i
|
2664
|
123 |
\item LCF system, 15, 26
|
|
124 |
\item level of a proof, 31
|
|
125 |
\item lifting, \bold{14}
|
|
126 |
\item {\ptt logic} class, 3, 6, 25
|
105
|
127 |
|
|
128 |
\indexspace
|
|
129 |
|
2664
|
130 |
\item major premise, \bold{21}
|
|
131 |
\item {\ptt Match} exception, 42
|
359
|
132 |
\item meta-assumptions
|
2664
|
133 |
\subitem syntax of, 22
|
|
134 |
\item meta-equality, \bold{5}, 25
|
|
135 |
\item meta-implication, \bold{5}, 7, 25
|
|
136 |
\item meta-quantifiers, \bold{5}, 8, 25
|
|
137 |
\item meta-rewriting, 43
|
|
138 |
\item mixfix declarations, 52, 53, 56
|
359
|
139 |
\item ML, i
|
2664
|
140 |
\item {\ptt ML} section, 47
|
|
141 |
\item {\ptt mp} theorem, 27
|
105
|
142 |
|
|
143 |
\indexspace
|
|
144 |
|
2664
|
145 |
\item {\ptt Nat} theory, 55
|
359
|
146 |
\item {\ptt nat} type, 1, 3
|
2664
|
147 |
\item {\ptt not_def} theorem, 44
|
|
148 |
\item {\ptt notE} theorem, \bold{45}, 58
|
|
149 |
\item {\ptt notI} theorem, \bold{44}, 58
|
105
|
150 |
|
|
151 |
\indexspace
|
|
152 |
|
359
|
153 |
\item {\ptt o} type, 1, 4
|
2664
|
154 |
\item {\ptt ORELSE}, 37
|
|
155 |
\item overloading, \bold{4}, 53
|
105
|
156 |
|
|
157 |
\indexspace
|
|
158 |
|
2664
|
159 |
\item parameters, \bold{8}, 33
|
|
160 |
\subitem lifting over, 15
|
|
161 |
\item {\ptt Prolog} theory, 61
|
|
162 |
\item Prolog interpreter, \bold{60}
|
|
163 |
\item proof state, 16
|
359
|
164 |
\item proofs
|
2664
|
165 |
\subitem commands for, 30
|
|
166 |
\item {\ptt PROP} symbol, 26
|
|
167 |
\item {\ptt prop} type, 6, 25, 26
|
|
168 |
\item {\ptt prth}, 27
|
|
169 |
\item {\ptt prthq}, 27, 28
|
|
170 |
\item {\ptt prths}, 27
|
|
171 |
\item {\ptt Pure} theory, 47
|
359
|
172 |
|
|
173 |
\indexspace
|
|
174 |
|
2664
|
175 |
\item quantifiers, 5, 8, 33
|
105
|
176 |
|
|
177 |
\indexspace
|
|
178 |
|
2664
|
179 |
\item {\ptt read_instantiate}, 29
|
|
180 |
\item {\ptt refl} theorem, 29
|
|
181 |
\item {\ptt REPEAT}, 33, 37, 62, 64
|
|
182 |
\item {\ptt res_inst_tac}, 57, 60
|
|
183 |
\item reserved words, 24
|
|
184 |
\item resolution, 10, \bold{12}
|
359
|
185 |
\subitem in backward proof, 15
|
2664
|
186 |
\subitem with instantiation, 57
|
|
187 |
\item {\ptt resolve_tac}, 30, 31, 46, 58
|
|
188 |
\item {\ptt result}, 30, 42, 46
|
|
189 |
\item {\ptt rewrite_goals_tac}, 44
|
|
190 |
\item {\ptt rewrite_rule}, 45, 46
|
|
191 |
\item {\ptt RL}, 29
|
|
192 |
\item {\ptt RLN}, 29
|
|
193 |
\item {\ptt RS}, 27, 29, 46
|
|
194 |
\item {\ptt RSN}, 27, 29
|
105
|
195 |
\item rules
|
2664
|
196 |
\subitem declaring, 48
|
|
197 |
\subitem derived, 13, \bold{22}, 41, 43
|
|
198 |
\subitem destruction, 21
|
|
199 |
\subitem elimination, 21
|
359
|
200 |
\subitem propositional, 6
|
2664
|
201 |
\subitem quantifier, 8
|
105
|
202 |
|
|
203 |
\indexspace
|
|
204 |
|
|
205 |
\item search
|
2664
|
206 |
\subitem depth-first, 63
|
|
207 |
\item signatures, \bold{9}
|
|
208 |
\item {\ptt simp_tac}, 60
|
|
209 |
\item simplification, 59
|
|
210 |
\item simplification sets, 59
|
|
211 |
\item sort constraints, 25
|
|
212 |
\item sorts, \bold{5}
|
|
213 |
\item {\ptt spec} theorem, 28, 36, 37
|
|
214 |
\item {\ptt standard}, 27
|
|
215 |
\item substitution, \bold{8}
|
|
216 |
\item {\ptt Suc_inject}, 58
|
|
217 |
\item {\ptt Suc_neq_0}, 58
|
359
|
218 |
\item syntax
|
2664
|
219 |
\subitem of types and terms, 25
|
105
|
220 |
|
|
221 |
\indexspace
|
|
222 |
|
2664
|
223 |
\item tacticals, \bold{19}, 37
|
|
224 |
\item tactics, \bold{19}
|
|
225 |
\subitem assumption, 29
|
|
226 |
\subitem resolution, 30
|
359
|
227 |
\item {\ptt term} class, 3
|
105
|
228 |
\item terms
|
2664
|
229 |
\subitem syntax of, 1, \bold{25}
|
105
|
230 |
\item theorems
|
2664
|
231 |
\subitem basic operations on, \bold{26}
|
|
232 |
\subitem printing of, 27
|
|
233 |
\item theories, \bold{9}
|
|
234 |
\subitem defining, 47--57
|
|
235 |
\item {\ptt thm} ML type, 26
|
|
236 |
\item {\ptt topthm}, 42
|
|
237 |
\item {\ptt Trueprop} constant, 6, 7, 25
|
|
238 |
\item type constraints, 25
|
359
|
239 |
\item type constructors, 1
|
2664
|
240 |
\item type identifiers, 24
|
|
241 |
\item type synonyms, \bold{51}
|
359
|
242 |
\item types
|
2664
|
243 |
\subitem declaring, \bold{49}
|
359
|
244 |
\subitem function, 1
|
|
245 |
\subitem higher, \bold{5}
|
105
|
246 |
\subitem polymorphic, \bold{3}
|
|
247 |
\subitem simple, \bold{1}
|
2664
|
248 |
\subitem syntax of, 1, \bold{25}
|
105
|
249 |
|
|
250 |
\indexspace
|
|
251 |
|
2664
|
252 |
\item {\ptt undo}, 30
|
105
|
253 |
\item unification
|
2664
|
254 |
\subitem higher-order, \bold{11}, 58
|
359
|
255 |
\subitem incompleteness of, 11
|
2664
|
256 |
\item unknowns, 10, 24, 33
|
|
257 |
\subitem function, \bold{11}, 28, 33
|
|
258 |
\item {\ptt use_thy}, \bold{47}
|
105
|
259 |
|
|
260 |
\indexspace
|
|
261 |
|
|
262 |
\item variables
|
2664
|
263 |
\subitem bound, 8
|
105
|
264 |
|
|
265 |
\end{theindex}
|