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