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 + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace. |
3 ;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace. |
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" |
44 "case" |
46 "case" |
45 "cd" |
47 "cd" |
46 "chapter" |
48 "chapter" |
47 "class" |
49 "class" |
48 "class_deps" |
50 "class_deps" |
49 "class_interpret" |
|
50 "class_interpretation" |
|
51 "class_locale" |
|
52 "classes" |
51 "classes" |
53 "classrel" |
52 "classrel" |
54 "code_abort" |
53 "code_abort" |
55 "code_class" |
54 "code_class" |
56 "code_const" |
55 "code_const" |
117 "init_toplevel" |
116 "init_toplevel" |
118 "instance" |
117 "instance" |
119 "instantiation" |
118 "instantiation" |
120 "interpret" |
119 "interpret" |
121 "interpretation" |
120 "interpretation" |
122 "invoke" |
|
123 "judgment" |
121 "judgment" |
124 "kill" |
122 "kill" |
125 "kill_thy" |
123 "kill_thy" |
126 "lemma" |
124 "lemma" |
127 "lemmas" |
125 "lemmas" |
170 "print_configs" |
168 "print_configs" |
171 "print_context" |
169 "print_context" |
172 "print_drafts" |
170 "print_drafts" |
173 "print_facts" |
171 "print_facts" |
174 "print_induct_rules" |
172 "print_induct_rules" |
175 "print_interps" |
|
176 "print_locale" |
173 "print_locale" |
177 "print_locales" |
174 "print_locales" |
178 "print_methods" |
175 "print_methods" |
179 "print_orders" |
176 "print_orders" |
180 "print_rules" |
177 "print_rules" |
310 "uses" |
307 "uses" |
311 "where")) |
308 "where")) |
312 |
309 |
313 (defconst isar-keywords-control |
310 (defconst isar-keywords-control |
314 '("Isabelle\\.command" |
311 '("Isabelle\\.command" |
|
312 "Isar\\.begin_document" |
315 "Isar\\.command" |
313 "Isar\\.command" |
|
314 "Isar\\.define_command" |
|
315 "Isar\\.edit_document" |
|
316 "Isar\\.end_document" |
316 "Isar\\.insert" |
317 "Isar\\.insert" |
317 "Isar\\.remove" |
318 "Isar\\.remove" |
318 "ProofGeneral\\.inform_file_processed" |
319 "ProofGeneral\\.inform_file_processed" |
319 "ProofGeneral\\.inform_file_retracted" |
320 "ProofGeneral\\.inform_file_retracted" |
320 "ProofGeneral\\.kill_proof" |
321 "ProofGeneral\\.kill_proof" |
367 "print_configs" |
368 "print_configs" |
368 "print_context" |
369 "print_context" |
369 "print_drafts" |
370 "print_drafts" |
370 "print_facts" |
371 "print_facts" |
371 "print_induct_rules" |
372 "print_induct_rules" |
372 "print_interps" |
|
373 "print_locale" |
373 "print_locale" |
374 "print_locales" |
374 "print_locales" |
375 "print_methods" |
375 "print_methods" |
376 "print_orders" |
376 "print_orders" |
377 "print_rules" |
377 "print_rules" |
421 "automaton" |
421 "automaton" |
422 "axclass" |
422 "axclass" |
423 "axiomatization" |
423 "axiomatization" |
424 "axioms" |
424 "axioms" |
425 "class" |
425 "class" |
426 "class_locale" |
|
427 "classes" |
426 "classes" |
428 "classrel" |
427 "classrel" |
429 "code_abort" |
428 "code_abort" |
430 "code_class" |
429 "code_class" |
431 "code_const" |
430 "code_const" |
505 (defconst isar-keywords-theory-script |
504 (defconst isar-keywords-theory-script |
506 '("inductive_cases")) |
505 '("inductive_cases")) |
507 |
506 |
508 (defconst isar-keywords-theory-goal |
507 (defconst isar-keywords-theory-goal |
509 '("ax_specification" |
508 '("ax_specification" |
510 "class_interpretation" |
|
511 "corollary" |
509 "corollary" |
512 "cpodef" |
510 "cpodef" |
513 "function" |
511 "function" |
514 "instance" |
512 "instance" |
515 "interpretation" |
513 "interpretation" |
544 '("sect" |
542 '("sect" |
545 "subsect" |
543 "subsect" |
546 "subsubsect")) |
544 "subsubsect")) |
547 |
545 |
548 (defconst isar-keywords-proof-goal |
546 (defconst isar-keywords-proof-goal |
549 '("class_interpret" |
547 '("have" |
550 "have" |
|
551 "hence" |
548 "hence" |
552 "interpret" |
549 "interpret")) |
553 "invoke")) |
|
554 |
550 |
555 (defconst isar-keywords-proof-block |
551 (defconst isar-keywords-proof-block |
556 '("next" |
552 '("next" |
557 "proof")) |
553 "proof")) |
558 |
554 |