equal
deleted
inserted
replaced
1 ;; |
1 ;; |
2 ;; Keyword classification tables for Isabelle/Isar. |
2 ;; Keyword classification tables for Isabelle/Isar. |
3 ;; Generated from HOL + Pure + Pure-ProofGeneral + HOL-Nominal-test. |
3 ;; Generated from HOL + Pure + Pure-ProofGeneral + HOL-Nominal-test + HOL-Nominal. |
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 '("\\." |
26 "also" |
26 "also" |
27 "apply" |
27 "apply" |
28 "apply_end" |
28 "apply_end" |
29 "arities" |
29 "arities" |
30 "assume" |
30 "assume" |
|
31 "atom_decl" |
31 "atp_info" |
32 "atp_info" |
32 "atp_kill" |
33 "atp_kill" |
33 "atp_messages" |
34 "atp_messages" |
34 "atp_minimize" |
35 "atp_minimize" |
35 "attribute_setup" |
36 "attribute_setup" |
82 "disable_pr" |
83 "disable_pr" |
83 "display_drafts" |
84 "display_drafts" |
84 "done" |
85 "done" |
85 "enable_pr" |
86 "enable_pr" |
86 "end" |
87 "end" |
|
88 "equivariance" |
87 "exit" |
89 "exit" |
88 "export_code" |
90 "export_code" |
89 "extract" |
91 "extract" |
90 "extract_type" |
92 "extract_type" |
91 "finalconsts" |
93 "finalconsts" |
126 "moreover" |
128 "moreover" |
127 "next" |
129 "next" |
128 "no_notation" |
130 "no_notation" |
129 "no_syntax" |
131 "no_syntax" |
130 "no_translations" |
132 "no_translations" |
|
133 "nominal_datatype" |
|
134 "nominal_inductive" |
|
135 "nominal_inductive2" |
|
136 "nominal_primrec" |
131 "nonterminals" |
137 "nonterminals" |
132 "normal_form" |
138 "normal_form" |
133 "notation" |
139 "notation" |
134 "note" |
140 "note" |
135 "obtain" |
141 "obtain" |
249 (defconst isar-keywords-minor |
255 (defconst isar-keywords-minor |
250 '("advanced" |
256 '("advanced" |
251 "and" |
257 "and" |
252 "assumes" |
258 "assumes" |
253 "attach" |
259 "attach" |
|
260 "avoids" |
254 "begin" |
261 "begin" |
255 "binder" |
262 "binder" |
256 "congs" |
263 "congs" |
257 "constrains" |
264 "constrains" |
258 "contains" |
265 "contains" |
395 |
402 |
396 (defconst isar-keywords-theory-decl |
403 (defconst isar-keywords-theory-decl |
397 '("ML" |
404 '("ML" |
398 "abbreviation" |
405 "abbreviation" |
399 "arities" |
406 "arities" |
|
407 "atom_decl" |
400 "attribute_setup" |
408 "attribute_setup" |
401 "axclass" |
409 "axclass" |
402 "axiomatization" |
410 "axiomatization" |
403 "axioms" |
411 "axioms" |
404 "class" |
412 "class" |
427 "declare" |
435 "declare" |
428 "defaultsort" |
436 "defaultsort" |
429 "defer_recdef" |
437 "defer_recdef" |
430 "definition" |
438 "definition" |
431 "defs" |
439 "defs" |
|
440 "equivariance" |
432 "extract" |
441 "extract" |
433 "extract_type" |
442 "extract_type" |
434 "finalconsts" |
443 "finalconsts" |
435 "fun" |
444 "fun" |
436 "global" |
445 "global" |
445 "locale" |
454 "locale" |
446 "method_setup" |
455 "method_setup" |
447 "no_notation" |
456 "no_notation" |
448 "no_syntax" |
457 "no_syntax" |
449 "no_translations" |
458 "no_translations" |
|
459 "nominal_datatype" |
450 "nonterminals" |
460 "nonterminals" |
451 "notation" |
461 "notation" |
452 "oracle" |
462 "oracle" |
453 "overloading" |
463 "overloading" |
454 "parse_ast_translation" |
464 "parse_ast_translation" |
485 "corollary" |
495 "corollary" |
486 "function" |
496 "function" |
487 "instance" |
497 "instance" |
488 "interpretation" |
498 "interpretation" |
489 "lemma" |
499 "lemma" |
|
500 "nominal_inductive" |
|
501 "nominal_inductive2" |
|
502 "nominal_primrec" |
490 "prove" |
503 "prove" |
491 "quotient" |
504 "quotient" |
492 "recdef_tc" |
505 "recdef_tc" |
493 "rep_datatype" |
506 "rep_datatype" |
494 "specification" |
507 "specification" |