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" |
204 "typedef" |
205 "typedef" |
205 "types" |
206 "types" |
206 "types_code" |
207 "types_code" |
207 "ultimately" |
208 "ultimately" |
208 "undo" |
209 "undo" |
|
210 "undo_end" |
209 "undos_proof" |
211 "undos_proof" |
210 "unfolding" |
212 "unfolding" |
211 "update_thy" |
213 "update_thy" |
212 "update_thy_only" |
214 "update_thy_only" |
213 "use" |
215 "use" |
281 "init_toplevel" |
283 "init_toplevel" |
282 "kill" |
284 "kill" |
283 "quit" |
285 "quit" |
284 "redo" |
286 "redo" |
285 "undo" |
287 "undo" |
|
288 "undo_end" |
286 "undos_proof")) |
289 "undos_proof")) |
287 |
290 |
288 (defconst isar-keywords-diag |
291 (defconst isar-keywords-diag |
289 '("ML" |
292 '("ML" |
290 "ML_command" |
293 "ML_command" |
371 "axiomatization" |
374 "axiomatization" |
372 "axioms" |
375 "axioms" |
373 "class" |
376 "class" |
374 "classes" |
377 "classes" |
375 "classrel" |
378 "classrel" |
|
379 "code_abstype" |
376 "code_class" |
380 "code_class" |
377 "code_const" |
381 "code_const" |
378 "code_constname" |
382 "code_constname" |
|
383 "code_constsubst" |
379 "code_instance" |
384 "code_instance" |
380 "code_instname" |
385 "code_instname" |
381 "code_library" |
386 "code_library" |
382 "code_module" |
387 "code_module" |
383 "code_type" |
388 "code_type" |
437 '("declare" |
442 '("declare" |
438 "inductive_cases")) |
443 "inductive_cases")) |
439 |
444 |
440 (defconst isar-keywords-theory-goal |
445 (defconst isar-keywords-theory-goal |
441 '("ax_specification" |
446 '("ax_specification" |
442 "code_simtype" |
|
443 "corollary" |
447 "corollary" |
444 "function" |
448 "function" |
445 "instance" |
449 "instance" |
446 "interpretation" |
450 "interpretation" |
447 "lemma" |
451 "lemma" |