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