equal
deleted
inserted
replaced
41 "class" |
41 "class" |
42 "class_deps" |
42 "class_deps" |
43 "classes" |
43 "classes" |
44 "classrel" |
44 "classrel" |
45 "clear_undos" |
45 "clear_undos" |
|
46 "code_abstype" |
46 "code_class" |
47 "code_class" |
47 "code_const" |
48 "code_const" |
48 "code_constname" |
49 "code_constname" |
|
50 "code_constsubst" |
49 "code_gen" |
51 "code_gen" |
50 "code_instance" |
52 "code_instance" |
51 "code_instname" |
53 "code_instname" |
52 "code_library" |
54 "code_library" |
53 "code_module" |
55 "code_module" |
54 "code_simtype" |
|
55 "code_type" |
56 "code_type" |
56 "code_typename" |
57 "code_typename" |
57 "coinductive" |
58 "coinductive" |
58 "commit" |
59 "commit" |
59 "const_syntax" |
60 "const_syntax" |
208 "typedef" |
209 "typedef" |
209 "types" |
210 "types" |
210 "types_code" |
211 "types_code" |
211 "ultimately" |
212 "ultimately" |
212 "undo" |
213 "undo" |
|
214 "undo_end" |
213 "undos_proof" |
215 "undos_proof" |
214 "unfolding" |
216 "unfolding" |
215 "update_thy" |
217 "update_thy" |
216 "update_thy_only" |
218 "update_thy_only" |
217 "use" |
219 "use" |
302 "init_toplevel" |
304 "init_toplevel" |
303 "kill" |
305 "kill" |
304 "quit" |
306 "quit" |
305 "redo" |
307 "redo" |
306 "undo" |
308 "undo" |
|
309 "undo_end" |
307 "undos_proof")) |
310 "undos_proof")) |
308 |
311 |
309 (defconst isar-keywords-diag |
312 (defconst isar-keywords-diag |
310 '("ML" |
313 '("ML" |
311 "ML_command" |
314 "ML_command" |
392 "axiomatization" |
395 "axiomatization" |
393 "axioms" |
396 "axioms" |
394 "class" |
397 "class" |
395 "classes" |
398 "classes" |
396 "classrel" |
399 "classrel" |
|
400 "code_abstype" |
397 "code_class" |
401 "code_class" |
398 "code_const" |
402 "code_const" |
399 "code_constname" |
403 "code_constname" |
|
404 "code_constsubst" |
400 "code_instance" |
405 "code_instance" |
401 "code_instname" |
406 "code_instname" |
402 "code_library" |
407 "code_library" |
403 "code_module" |
408 "code_module" |
404 "code_type" |
409 "code_type" |
460 '("declare" |
465 '("declare" |
461 "inductive_cases")) |
466 "inductive_cases")) |
462 |
467 |
463 (defconst isar-keywords-theory-goal |
468 (defconst isar-keywords-theory-goal |
464 '("ax_specification" |
469 '("ax_specification" |
465 "code_simtype" |
|
466 "corollary" |
470 "corollary" |
467 "cpodef" |
471 "cpodef" |
468 "function" |
472 "function" |
469 "instance" |
473 "instance" |
470 "interpretation" |
474 "interpretation" |