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 + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP. |
3 ;; Generated from Pure + HOL + HOLCF + HOL-Boogie + HOL-Library + HOL-Nominal + HOL-Statespace + HOL-SPARK + HOL-TPTP + HOL-HOL_Light. |
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 '("\\." |
106 "hence" |
106 "hence" |
107 "hide_class" |
107 "hide_class" |
108 "hide_const" |
108 "hide_const" |
109 "hide_fact" |
109 "hide_fact" |
110 "hide_type" |
110 "hide_type" |
|
111 "import_const_map" |
|
112 "import_file" |
111 "import_tptp" |
113 "import_tptp" |
|
114 "import_type_map" |
112 "include" |
115 "include" |
113 "including" |
116 "including" |
114 "inductive" |
117 "inductive" |
115 "inductive_cases" |
118 "inductive_cases" |
116 "inductive_set" |
119 "inductive_set" |
489 "fun" |
492 "fun" |
490 "hide_class" |
493 "hide_class" |
491 "hide_const" |
494 "hide_const" |
492 "hide_fact" |
495 "hide_fact" |
493 "hide_type" |
496 "hide_type" |
|
497 "import_const_map" |
|
498 "import_file" |
494 "import_tptp" |
499 "import_tptp" |
|
500 "import_type_map" |
495 "inductive" |
501 "inductive" |
496 "inductive_set" |
502 "inductive_set" |
497 "instantiation" |
503 "instantiation" |
498 "judgment" |
504 "judgment" |
499 "lemmas" |
505 "lemmas" |