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