equal
deleted
inserted
replaced
1 ;; |
1 ;; |
2 ;; Keyword classification tables for Isabelle/Isar. |
2 ;; Keyword classification tables for Isabelle/Isar. |
3 ;; Generated from Pure + HOL + Pure-ProofGeneral + HOL-Command. |
3 ;; Generated from Pure + Pure-ProofGeneral + HOL + HOL-Command. |
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** |
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** |
5 ;; |
5 ;; |
6 |
6 |
7 (defconst isar-keywords-major |
7 (defconst isar-keywords-major |
8 '("\\." |
8 '("\\." |
95 "finally" |
95 "finally" |
96 "find_consts" |
96 "find_consts" |
97 "find_theorems" |
97 "find_theorems" |
98 "fix" |
98 "fix" |
99 "foobar" |
99 "foobar" |
|
100 "foobar_goal" |
|
101 "foobar_prove" |
|
102 "foobar_trace" |
100 "from" |
103 "from" |
101 "full_prf" |
104 "full_prf" |
102 "fun" |
105 "fun" |
103 "function" |
106 "function" |
104 "global" |
107 "global" |
195 "rep_datatype" |
198 "rep_datatype" |
196 "sect" |
199 "sect" |
197 "section" |
200 "section" |
198 "setup" |
201 "setup" |
199 "show" |
202 "show" |
200 "simple_induct" |
203 "simple_inductive" |
201 "simproc_setup" |
204 "simproc_setup" |
202 "sledgehammer" |
205 "sledgehammer" |
203 "sorry" |
206 "sorry" |
204 "specification" |
207 "specification" |
205 "subclass" |
208 "subclass" |
431 "definition" |
434 "definition" |
432 "defs" |
435 "defs" |
433 "extract" |
436 "extract" |
434 "extract_type" |
437 "extract_type" |
435 "finalconsts" |
438 "finalconsts" |
|
439 "foobar" |
|
440 "foobar_trace" |
436 "fun" |
441 "fun" |
437 "global" |
442 "global" |
438 "hide" |
443 "hide" |
439 "inductive" |
444 "inductive" |
440 "inductive_set" |
445 "inductive_set" |
462 "realizers" |
467 "realizers" |
463 "recdef" |
468 "recdef" |
464 "record" |
469 "record" |
465 "refute_params" |
470 "refute_params" |
466 "setup" |
471 "setup" |
467 "simple_induct" |
472 "simple_inductive" |
468 "simproc_setup" |
473 "simproc_setup" |
469 "syntax" |
474 "syntax" |
470 "text" |
475 "text" |
471 "text_raw" |
476 "text_raw" |
472 "theorems" |
477 "theorems" |
482 |
487 |
483 (defconst isar-keywords-theory-goal |
488 (defconst isar-keywords-theory-goal |
484 '("ax_specification" |
489 '("ax_specification" |
485 "code_pred" |
490 "code_pred" |
486 "corollary" |
491 "corollary" |
487 "foobar" |
492 "foobar_goal" |
|
493 "foobar_prove" |
488 "function" |
494 "function" |
489 "instance" |
495 "instance" |
490 "interpretation" |
496 "interpretation" |
491 "lemma" |
497 "lemma" |
492 "recdef_tc" |
498 "recdef_tc" |