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 + HOL-ex. |
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 '("\\." |
16 "Isar\\.insert" |
16 "Isar\\.insert" |
17 "Isar\\.remove" |
17 "Isar\\.remove" |
18 "ML" |
18 "ML" |
19 "ML_command" |
19 "ML_command" |
20 "ML_prf" |
20 "ML_prf" |
21 "ML_test" |
|
22 "ML_val" |
21 "ML_val" |
23 "ProofGeneral\\.inform_file_processed" |
22 "ProofGeneral\\.inform_file_processed" |
24 "ProofGeneral\\.inform_file_retracted" |
23 "ProofGeneral\\.inform_file_retracted" |
25 "ProofGeneral\\.kill_proof" |
24 "ProofGeneral\\.kill_proof" |
26 "ProofGeneral\\.process_pgip" |
25 "ProofGeneral\\.process_pgip" |
35 "atom_decl" |
34 "atom_decl" |
36 "atp_info" |
35 "atp_info" |
37 "atp_kill" |
36 "atp_kill" |
38 "atp_messages" |
37 "atp_messages" |
39 "attribute_setup" |
38 "attribute_setup" |
40 "automaton" |
|
41 "ax_specification" |
39 "ax_specification" |
42 "axclass" |
40 "axclass" |
43 "axiomatization" |
41 "axiomatization" |
44 "axioms" |
42 "axioms" |
45 "back" |
43 "back" |
61 "code_instance" |
59 "code_instance" |
62 "code_library" |
60 "code_library" |
63 "code_module" |
61 "code_module" |
64 "code_modulename" |
62 "code_modulename" |
65 "code_monad" |
63 "code_monad" |
|
64 "code_pred" |
66 "code_reserved" |
65 "code_reserved" |
67 "code_thms" |
66 "code_thms" |
68 "code_type" |
67 "code_type" |
69 "coinductive" |
68 "coinductive" |
70 "coinductive_set" |
69 "coinductive_set" |
72 "constdefs" |
71 "constdefs" |
73 "consts" |
72 "consts" |
74 "consts_code" |
73 "consts_code" |
75 "context" |
74 "context" |
76 "corollary" |
75 "corollary" |
77 "cpodef" |
|
78 "datatype" |
76 "datatype" |
79 "declaration" |
77 "declaration" |
80 "declare" |
78 "declare" |
81 "def" |
79 "def" |
82 "defaultsort" |
80 "defaultsort" |
84 "defer_recdef" |
82 "defer_recdef" |
85 "definition" |
83 "definition" |
86 "defs" |
84 "defs" |
87 "disable_pr" |
85 "disable_pr" |
88 "display_drafts" |
86 "display_drafts" |
89 "domain" |
|
90 "done" |
87 "done" |
91 "enable_pr" |
88 "enable_pr" |
92 "end" |
89 "end" |
93 "equivariance" |
90 "equivariance" |
94 "exit" |
91 "exit" |
98 "finalconsts" |
95 "finalconsts" |
99 "finally" |
96 "finally" |
100 "find_consts" |
97 "find_consts" |
101 "find_theorems" |
98 "find_theorems" |
102 "fix" |
99 "fix" |
103 "fixpat" |
|
104 "fixrec" |
|
105 "from" |
100 "from" |
106 "full_prf" |
101 "full_prf" |
107 "fun" |
102 "fun" |
108 "function" |
103 "function" |
109 "global" |
104 "global" |
149 "oops" |
144 "oops" |
150 "oracle" |
145 "oracle" |
151 "overloading" |
146 "overloading" |
152 "parse_ast_translation" |
147 "parse_ast_translation" |
153 "parse_translation" |
148 "parse_translation" |
154 "pcpodef" |
|
155 "pr" |
149 "pr" |
156 "prefer" |
150 "prefer" |
157 "presume" |
151 "presume" |
158 "pretty_setmargin" |
152 "pretty_setmargin" |
159 "prf" |
153 "prf" |
253 "with" |
247 "with" |
254 "{" |
248 "{" |
255 "}")) |
249 "}")) |
256 |
250 |
257 (defconst isar-keywords-minor |
251 (defconst isar-keywords-minor |
258 '("actions" |
252 '("advanced" |
259 "advanced" |
|
260 "and" |
253 "and" |
261 "assumes" |
254 "assumes" |
262 "attach" |
255 "attach" |
263 "avoids" |
256 "avoids" |
264 "begin" |
257 "begin" |
265 "binder" |
258 "binder" |
266 "compose" |
|
267 "congs" |
259 "congs" |
268 "constrains" |
260 "constrains" |
269 "contains" |
261 "contains" |
270 "defines" |
262 "defines" |
271 "file" |
263 "file" |
272 "fixes" |
264 "fixes" |
273 "for" |
265 "for" |
274 "hide_action" |
|
275 "hints" |
266 "hints" |
276 "identifier" |
267 "identifier" |
277 "if" |
268 "if" |
278 "imports" |
269 "imports" |
279 "in" |
270 "in" |
280 "infix" |
271 "infix" |
281 "infixl" |
272 "infixl" |
282 "infixr" |
273 "infixr" |
283 "initially" |
|
284 "inputs" |
|
285 "internals" |
|
286 "is" |
274 "is" |
287 "lazy" |
|
288 "module_name" |
275 "module_name" |
289 "monos" |
276 "monos" |
290 "morphisms" |
277 "morphisms" |
291 "notes" |
278 "notes" |
292 "obtains" |
279 "obtains" |
293 "open" |
280 "open" |
294 "output" |
281 "output" |
295 "outputs" |
|
296 "overloaded" |
282 "overloaded" |
297 "permissive" |
283 "permissive" |
298 "post" |
|
299 "pre" |
|
300 "rename" |
|
301 "restrict" |
|
302 "shows" |
284 "shows" |
303 "signature" |
|
304 "states" |
|
305 "structure" |
285 "structure" |
306 "to" |
|
307 "transitions" |
|
308 "transrel" |
|
309 "unchecked" |
286 "unchecked" |
310 "uses" |
287 "uses" |
311 "where")) |
288 "where")) |
312 |
289 |
313 (defconst isar-keywords-control |
290 (defconst isar-keywords-control |
417 "subsection" |
394 "subsection" |
418 "subsubsection")) |
395 "subsubsection")) |
419 |
396 |
420 (defconst isar-keywords-theory-decl |
397 (defconst isar-keywords-theory-decl |
421 '("ML" |
398 '("ML" |
422 "ML_test" |
|
423 "abbreviation" |
399 "abbreviation" |
424 "arities" |
400 "arities" |
425 "atom_decl" |
401 "atom_decl" |
426 "attribute_setup" |
402 "attribute_setup" |
427 "automaton" |
|
428 "axclass" |
403 "axclass" |
429 "axiomatization" |
404 "axiomatization" |
430 "axioms" |
405 "axioms" |
431 "class" |
406 "class" |
432 "classes" |
407 "classes" |
454 "declare" |
429 "declare" |
455 "defaultsort" |
430 "defaultsort" |
456 "defer_recdef" |
431 "defer_recdef" |
457 "definition" |
432 "definition" |
458 "defs" |
433 "defs" |
459 "domain" |
|
460 "equivariance" |
434 "equivariance" |
461 "extract" |
435 "extract" |
462 "extract_type" |
436 "extract_type" |
463 "finalconsts" |
437 "finalconsts" |
464 "fixpat" |
|
465 "fixrec" |
|
466 "fun" |
438 "fun" |
467 "global" |
439 "global" |
468 "hide" |
440 "hide" |
469 "inductive" |
441 "inductive" |
470 "inductive_set" |
442 "inductive_set" |
511 (defconst isar-keywords-theory-script |
483 (defconst isar-keywords-theory-script |
512 '("inductive_cases")) |
484 '("inductive_cases")) |
513 |
485 |
514 (defconst isar-keywords-theory-goal |
486 (defconst isar-keywords-theory-goal |
515 '("ax_specification" |
487 '("ax_specification" |
|
488 "code_pred" |
516 "corollary" |
489 "corollary" |
517 "cpodef" |
|
518 "function" |
490 "function" |
519 "instance" |
491 "instance" |
520 "interpretation" |
492 "interpretation" |
521 "lemma" |
493 "lemma" |
522 "nominal_inductive" |
494 "nominal_inductive" |
523 "nominal_inductive2" |
495 "nominal_inductive2" |
524 "nominal_primrec" |
496 "nominal_primrec" |
525 "pcpodef" |
|
526 "recdef_tc" |
497 "recdef_tc" |
527 "rep_datatype" |
498 "rep_datatype" |
528 "specification" |
499 "specification" |
529 "subclass" |
500 "subclass" |
530 "sublocale" |
501 "sublocale" |