equal
deleted
inserted
replaced
36 "class_deps" |
36 "class_deps" |
37 "classes" |
37 "classes" |
38 "classrel" |
38 "classrel" |
39 "codatatype" |
39 "codatatype" |
40 "code_datatype" |
40 "code_datatype" |
|
41 "code_library" |
|
42 "code_module" |
41 "coinductive" |
43 "coinductive" |
42 "commit" |
44 "commit" |
43 "constdefs" |
45 "constdefs" |
44 "consts" |
46 "consts" |
|
47 "consts_code" |
45 "context" |
48 "context" |
46 "corollary" |
49 "corollary" |
47 "datatype" |
50 "datatype" |
48 "declaration" |
51 "declaration" |
49 "declare" |
52 "declare" |
75 "hide" |
78 "hide" |
76 "inductive" |
79 "inductive" |
77 "inductive_cases" |
80 "inductive_cases" |
78 "init_toplevel" |
81 "init_toplevel" |
79 "instance" |
82 "instance" |
|
83 "instance_proof" |
|
84 "instantiation" |
80 "interpret" |
85 "interpret" |
81 "interpretation" |
86 "interpretation" |
82 "invoke" |
87 "invoke" |
83 "judgment" |
88 "judgment" |
84 "kill" |
89 "kill" |
137 "print_translation" |
142 "print_translation" |
138 "proof" |
143 "proof" |
139 "prop" |
144 "prop" |
140 "pwd" |
145 "pwd" |
141 "qed" |
146 "qed" |
|
147 "quickcheck" |
|
148 "quickcheck_params" |
142 "quit" |
149 "quit" |
143 "realizability" |
150 "realizability" |
144 "realizers" |
151 "realizers" |
145 "redo" |
152 "redo" |
146 "remove_thy" |
153 "remove_thy" |
175 "txt_raw" |
182 "txt_raw" |
176 "typ" |
183 "typ" |
177 "typed_print_translation" |
184 "typed_print_translation" |
178 "typedecl" |
185 "typedecl" |
179 "types" |
186 "types" |
|
187 "types_code" |
180 "ultimately" |
188 "ultimately" |
181 "undo" |
189 "undo" |
182 "undos_proof" |
190 "undos_proof" |
183 "unfolding" |
191 "unfolding" |
184 "use" |
192 "use" |
185 "use_thy" |
193 "use_thy" |
186 "using" |
194 "using" |
|
195 "value" |
187 "welcome" |
196 "welcome" |
188 "with" |
197 "with" |
189 "{" |
198 "{" |
190 "}")) |
199 "}")) |
191 |
200 |
198 "binder" |
207 "binder" |
199 "case_eqns" |
208 "case_eqns" |
200 "con_defs" |
209 "con_defs" |
201 "concl" |
210 "concl" |
202 "constrains" |
211 "constrains" |
|
212 "contains" |
203 "defines" |
213 "defines" |
204 "domains" |
214 "domains" |
205 "elimination" |
215 "elimination" |
|
216 "file" |
206 "fixes" |
217 "fixes" |
207 "for" |
218 "for" |
208 "identifier" |
219 "identifier" |
209 "if" |
220 "if" |
210 "imports" |
221 "imports" |
214 "infix" |
225 "infix" |
215 "infixl" |
226 "infixl" |
216 "infixr" |
227 "infixr" |
217 "intros" |
228 "intros" |
218 "is" |
229 "is" |
|
230 "local_syntax" |
219 "monos" |
231 "monos" |
220 "notes" |
232 "notes" |
221 "obtains" |
233 "obtains" |
222 "open" |
234 "open" |
223 "output" |
235 "output" |
290 "print_theorems" |
302 "print_theorems" |
291 "print_theory" |
303 "print_theory" |
292 "print_trans_rules" |
304 "print_trans_rules" |
293 "prop" |
305 "prop" |
294 "pwd" |
306 "pwd" |
|
307 "quickcheck" |
295 "remove_thy" |
308 "remove_thy" |
296 "term" |
309 "term" |
297 "thm" |
310 "thm" |
298 "thm_deps" |
311 "thm_deps" |
299 "thy_deps" |
312 "thy_deps" |
300 "touch_child_thys" |
313 "touch_child_thys" |
301 "touch_thy" |
314 "touch_thy" |
302 "typ" |
315 "typ" |
303 "use" |
316 "use" |
304 "use_thy" |
317 "use_thy" |
|
318 "value" |
305 "welcome")) |
319 "welcome")) |
306 |
320 |
307 (defconst isar-keywords-theory-begin |
321 (defconst isar-keywords-theory-begin |
308 '("theory")) |
322 '("theory")) |
309 |
323 |
329 "class" |
343 "class" |
330 "classes" |
344 "classes" |
331 "classrel" |
345 "classrel" |
332 "codatatype" |
346 "codatatype" |
333 "code_datatype" |
347 "code_datatype" |
|
348 "code_library" |
|
349 "code_module" |
334 "coinductive" |
350 "coinductive" |
335 "constdefs" |
351 "constdefs" |
336 "consts" |
352 "consts" |
|
353 "consts_code" |
337 "context" |
354 "context" |
338 "datatype" |
355 "datatype" |
339 "declaration" |
356 "declaration" |
340 "declare" |
357 "declare" |
341 "defaultsort" |
358 "defaultsort" |
345 "extract_type" |
362 "extract_type" |
346 "finalconsts" |
363 "finalconsts" |
347 "global" |
364 "global" |
348 "hide" |
365 "hide" |
349 "inductive" |
366 "inductive" |
|
367 "instantiation" |
350 "judgment" |
368 "judgment" |
351 "lemmas" |
369 "lemmas" |
352 "local" |
370 "local" |
353 "locale" |
371 "locale" |
354 "method_setup" |
372 "method_setup" |
360 "parse_ast_translation" |
378 "parse_ast_translation" |
361 "parse_translation" |
379 "parse_translation" |
362 "primrec" |
380 "primrec" |
363 "print_ast_translation" |
381 "print_ast_translation" |
364 "print_translation" |
382 "print_translation" |
|
383 "quickcheck_params" |
365 "realizability" |
384 "realizability" |
366 "realizers" |
385 "realizers" |
367 "rep_datatype" |
386 "rep_datatype" |
368 "setup" |
387 "setup" |
369 "simproc_setup" |
388 "simproc_setup" |
373 "theorems" |
392 "theorems" |
374 "token_translation" |
393 "token_translation" |
375 "translations" |
394 "translations" |
376 "typed_print_translation" |
395 "typed_print_translation" |
377 "typedecl" |
396 "typedecl" |
378 "types")) |
397 "types" |
|
398 "types_code")) |
379 |
399 |
380 (defconst isar-keywords-theory-script |
400 (defconst isar-keywords-theory-script |
381 '("inductive_cases")) |
401 '("inductive_cases")) |
382 |
402 |
383 (defconst isar-keywords-theory-goal |
403 (defconst isar-keywords-theory-goal |
384 '("corollary" |
404 '("corollary" |
385 "instance" |
405 "instance" |
|
406 "instance_proof" |
386 "interpretation" |
407 "interpretation" |
387 "lemma" |
408 "lemma" |
388 "theorem")) |
409 "theorem")) |
389 |
410 |
390 (defconst isar-keywords-qed |
411 (defconst isar-keywords-qed |