equal
deleted
inserted
replaced
1 ;; |
1 ;; |
2 ;; Keyword classification tables for Isabelle/Isar. |
2 ;; Keyword classification tables for Isabelle/Isar. |
3 ;; Generated from Pure + Pure-ProofGeneral + FOL + ZF. |
3 ;; Generated from Pure + Pure-ProofGeneral + FOL + ZF. |
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** |
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** |
5 ;; |
5 ;; |
6 ;; $Id$ |
|
7 ;; |
|
8 |
6 |
9 (defconst isar-keywords-major |
7 (defconst isar-keywords-major |
10 '("\\." |
8 '("\\." |
11 "\\.\\." |
9 "\\.\\." |
12 "Isabelle\\.command" |
10 "Isabelle\\.command" |
|
11 "Isar\\.begin_document" |
13 "Isar\\.command" |
12 "Isar\\.command" |
|
13 "Isar\\.define_command" |
|
14 "Isar\\.edit_document" |
|
15 "Isar\\.end_document" |
14 "Isar\\.insert" |
16 "Isar\\.insert" |
15 "Isar\\.remove" |
17 "Isar\\.remove" |
16 "ML" |
18 "ML" |
17 "ML_command" |
19 "ML_command" |
18 "ML_prf" |
20 "ML_prf" |
87 "init_toplevel" |
89 "init_toplevel" |
88 "instance" |
90 "instance" |
89 "instantiation" |
91 "instantiation" |
90 "interpret" |
92 "interpret" |
91 "interpretation" |
93 "interpretation" |
92 "invoke" |
|
93 "judgment" |
94 "judgment" |
94 "kill" |
95 "kill" |
95 "kill_thy" |
96 "kill_thy" |
96 "lemma" |
97 "lemma" |
97 "lemmas" |
98 "lemmas" |
133 "print_configs" |
134 "print_configs" |
134 "print_context" |
135 "print_context" |
135 "print_drafts" |
136 "print_drafts" |
136 "print_facts" |
137 "print_facts" |
137 "print_induct_rules" |
138 "print_induct_rules" |
138 "print_interps" |
|
139 "print_locale" |
139 "print_locale" |
140 "print_locales" |
140 "print_locales" |
141 "print_methods" |
141 "print_methods" |
142 "print_rules" |
142 "print_rules" |
143 "print_simpset" |
143 "print_simpset" |
247 "uses" |
247 "uses" |
248 "where")) |
248 "where")) |
249 |
249 |
250 (defconst isar-keywords-control |
250 (defconst isar-keywords-control |
251 '("Isabelle\\.command" |
251 '("Isabelle\\.command" |
|
252 "Isar\\.begin_document" |
252 "Isar\\.command" |
253 "Isar\\.command" |
|
254 "Isar\\.define_command" |
|
255 "Isar\\.edit_document" |
|
256 "Isar\\.end_document" |
253 "Isar\\.insert" |
257 "Isar\\.insert" |
254 "Isar\\.remove" |
258 "Isar\\.remove" |
255 "ProofGeneral\\.inform_file_processed" |
259 "ProofGeneral\\.inform_file_processed" |
256 "ProofGeneral\\.inform_file_retracted" |
260 "ProofGeneral\\.inform_file_retracted" |
257 "ProofGeneral\\.kill_proof" |
261 "ProofGeneral\\.kill_proof" |
296 "print_configs" |
300 "print_configs" |
297 "print_context" |
301 "print_context" |
298 "print_drafts" |
302 "print_drafts" |
299 "print_facts" |
303 "print_facts" |
300 "print_induct_rules" |
304 "print_induct_rules" |
301 "print_interps" |
|
302 "print_locale" |
305 "print_locale" |
303 "print_locales" |
306 "print_locales" |
304 "print_methods" |
307 "print_methods" |
305 "print_rules" |
308 "print_rules" |
306 "print_simpset" |
309 "print_simpset" |
436 "subsubsect")) |
439 "subsubsect")) |
437 |
440 |
438 (defconst isar-keywords-proof-goal |
441 (defconst isar-keywords-proof-goal |
439 '("have" |
442 '("have" |
440 "hence" |
443 "hence" |
441 "interpret" |
444 "interpret")) |
442 "invoke")) |
|
443 |
445 |
444 (defconst isar-keywords-proof-block |
446 (defconst isar-keywords-proof-block |
445 '("next" |
447 '("next" |
446 "proof")) |
448 "proof")) |
447 |
449 |