| author | Walther Neuper <wneuper@ist.tugraz.at> |
| Sat, 05 Dec 2015 14:26:56 +0100 | |
| changeset 59179 | 91acbb24e371 |
| parent 58784 | 2373b4c61111 |
| permissions | -rw-r--r-- |
1 ;;
2 ;; Keyword classification tables for Isabelle/Isar.
3 ;; Generated from HOL + HOL-Auth + HOL-BNF_Examples + HOL-Bali + HOL-Decision_Procs + HOL-IMP + HOL-Imperative_HOL + HOL-Import + HOL-Library + HOL-Mutabelle + HOL-Nominal + HOL-Predicate_Compile_Examples + HOL-Proofs + HOL-Proofs-Extraction + HOL-SPARK + HOL-Statespace + HOL-TPTP + HOL-Word-SMT_Examples + HOL-ex + HOLCF + Pure.
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
5 ;;
7 (defconst isar-keywords-major
8 '("\\."
9 "\\.\\."
10 "Isabelle\\.command"
11 "ML"
12 "ML_command"
13 "ML_file"
14 "ML_prf"
15 "ML_val"
16 "ProofGeneral\\.inform_file_processed"
17 "ProofGeneral\\.inform_file_retracted"
18 "ProofGeneral\\.kill_proof"
19 "ProofGeneral\\.pr"
20 "ProofGeneral\\.process_pgip"
21 "ProofGeneral\\.restart"
22 "ProofGeneral\\.undo"
23 "SML_export"
24 "SML_file"
25 "SML_import"
26 "abbreviation"
27 "adhoc_overloading"
28 "also"
29 "apply"
30 "apply_end"
31 "approximate"
32 "assume"
33 "atom_decl"
34 "attribute_setup"
35 "axiomatization"
36 "back"
37 "bnf"
38 "bnf_axiomatization"
39 "boogie_file"
40 "bundle"
41 "by"
42 "cannot_undo"
43 "cartouche"
44 "case"
45 "case_of_simps"
46 "chapter"
47 "class"
48 "class_deps"
49 "codatatype"
50 "code_datatype"
51 "code_deps"
52 "code_identifier"
53 "code_monad"
54 "code_pred"
55 "code_printing"
56 "code_reflect"
57 "code_reserved"
58 "code_thms"
59 "coinductive"
60 "coinductive_set"
61 "commit"
62 "consts"
63 "context"
64 "corollary"
65 "cpodef"
66 "datatype"
67 "datatype_compat"
68 "datatype_new"
69 "declaration"
70 "declare"
71 "def"
72 "default_sort"
73 "defer"
74 "defer_recdef"
75 "definition"
76 "defs"
77 "disable_pr"
78 "display_drafts"
79 "domain"
80 "domain_isomorphism"
81 "domaindef"
82 "done"
83 "enable_pr"
84 "end"
85 "equivariance"
86 "exit"
87 "export_code"
88 "extract"
89 "extract_type"
90 "finally"
91 "find_consts"
92 "find_theorems"
93 "find_unused_assms"
94 "fix"
95 "fixrec"
96 "free_constructors"
97 "from"
98 "full_prf"
99 "fun"
100 "fun_cases"
101 "function"
102 "functor"
103 "guess"
104 "have"
105 "header"
106 "help"
107 "hence"
108 "hide_class"
109 "hide_const"
110 "hide_fact"
111 "hide_type"
112 "import_const_map"
113 "import_file"
114 "import_tptp"
115 "import_type_map"
116 "include"
117 "including"
118 "inductive"
119 "inductive_cases"
120 "inductive_set"
121 "inductive_simps"
122 "init_toplevel"
123 "instance"
124 "instantiation"
125 "interpret"
126 "interpretation"
127 "judgment"
128 "kill"
129 "kill_thy"
130 "lemma"
131 "lemmas"
132 "let"
133 "lift_definition"
134 "lifting_forget"
135 "lifting_update"
136 "linear_undo"
137 "local_setup"
138 "locale"
139 "locale_deps"
140 "method_setup"
141 "moreover"
142 "next"
143 "nitpick"
144 "nitpick_params"
145 "no_adhoc_overloading"
146 "no_notation"
147 "no_syntax"
148 "no_translations"
149 "no_type_notation"
150 "nominal_datatype"
151 "nominal_function"
152 "nominal_inductive"
153 "nominal_inductive2"
154 "nominal_primrec"
155 "nominal_termination"
156 "nonterminal"
157 "notation"
158 "note"
159 "notepad"
160 "obtain"
161 "oops"
162 "oracle"
163 "overloading"
164 "parse_ast_translation"
165 "parse_translation"
166 "partial_function"
167 "pcpodef"
168 "permanent_interpretation"
169 "pr"
170 "prefer"
171 "presume"
172 "pretty_setmargin"
173 "prf"
174 "primcorec"
175 "primcorecursive"
176 "primrec"
177 "print_ML_antiquotations"
178 "print_abbrevs"
179 "print_antiquotations"
180 "print_ast_translation"
181 "print_attributes"
182 "print_binds"
183 "print_bnfs"
184 "print_bundles"
185 "print_case_translations"
186 "print_cases"
187 "print_claset"
188 "print_classes"
189 "print_codeproc"
190 "print_codesetup"
191 "print_coercions"
192 "print_commands"
193 "print_context"
194 "print_defn_rules"
195 "print_dependencies"
196 "print_facts"
197 "print_induct_rules"
198 "print_inductives"
199 "print_interps"
200 "print_locale"
201 "print_locales"
202 "print_methods"
203 "print_options"
204 "print_orders"
205 "print_quot_maps"
206 "print_quotconsts"
207 "print_quotients"
208 "print_quotientsQ3"
209 "print_quotmapsQ3"
210 "print_rules"
211 "print_simpset"
212 "print_state"
213 "print_statement"
214 "print_syntax"
215 "print_term_bindings"
216 "print_theorems"
217 "print_theory"
218 "print_trans_rules"
219 "print_translation"
220 "proof"
221 "prop"
222 "qed"
223 "quickcheck"
224 "quickcheck_generator"
225 "quickcheck_params"
226 "quit"
227 "quotient_definition"
228 "quotient_type"
229 "realizability"
230 "realizers"
231 "recdef"
232 "recdef_tc"
233 "record"
234 "refute"
235 "refute_params"
236 "remove_thy"
237 "rep_datatype"
238 "schematic_corollary"
239 "schematic_lemma"
240 "schematic_theorem"
241 "sect"
242 "section"
243 "setup"
244 "setup_lifting"
245 "show"
246 "simproc_setup"
247 "simps_of_case"
248 "sledgehammer"
249 "sledgehammer_params"
250 "smt2_status"
251 "smt_status"
252 "solve_direct"
253 "sorry"
254 "spark_end"
255 "spark_open"
256 "spark_open_vcg"
257 "spark_proof_functions"
258 "spark_status"
259 "spark_types"
260 "spark_vc"
261 "specification"
262 "statespace"
263 "subclass"
264 "sublocale"
265 "subsect"
266 "subsection"
267 "subsubsect"
268 "subsubsection"
269 "syntax"
270 "syntax_declaration"
271 "term"
272 "term_cartouche"
273 "termination"
274 "text"
275 "text_cartouche"
276 "text_raw"
277 "then"
278 "theorem"
279 "theorems"
280 "theory"
281 "thm"
282 "thm_deps"
283 "thus"
284 "thy_deps"
285 "translations"
286 "try"
287 "try0"
288 "txt"
289 "txt_raw"
290 "typ"
291 "type_notation"
292 "type_synonym"
293 "typed_print_translation"
294 "typedecl"
295 "typedef"
296 "ultimately"
297 "undo"
298 "undos_proof"
299 "unfolding"
300 "unused_thms"
301 "use_thy"
302 "using"
303 "value"
304 "values"
305 "values_prolog"
306 "welcome"
307 "with"
308 "write"
309 "{"
310 "}"))
312 (defconst isar-keywords-minor
313 '("and"
314 "assumes"
315 "attach"
316 "avoids"
317 "begin"
318 "binder"
319 "binds"
320 "checking"
321 "class_instance"
322 "class_relation"
323 "code_module"
324 "congs"
325 "constant"
326 "constrains"
327 "datatypes"
328 "defines"
329 "defining"
330 "file"
331 "fixes"
332 "for"
333 "functions"
334 "hints"
335 "identifier"
336 "if"
337 "imports"
338 "in"
339 "includes"
340 "infix"
341 "infixl"
342 "infixr"
343 "is"
344 "keywords"
345 "lazy"
346 "module_name"
347 "monos"
348 "morphisms"
349 "notes"
350 "obtains"
351 "open"
352 "output"
353 "overloaded"
354 "parametric"
355 "permissive"
356 "pervasive"
357 "shows"
358 "structure"
359 "type_class"
360 "type_constructor"
361 "unchecked"
362 "unsafe"
363 "where"))
365 (defconst isar-keywords-control
366 '("Isabelle\\.command"
367 "ProofGeneral\\.inform_file_processed"
368 "ProofGeneral\\.inform_file_retracted"
369 "ProofGeneral\\.kill_proof"
370 "ProofGeneral\\.pr"
371 "ProofGeneral\\.process_pgip"
372 "ProofGeneral\\.restart"
373 "ProofGeneral\\.undo"
374 "cannot_undo"
375 "commit"
376 "disable_pr"
377 "enable_pr"
378 "exit"
379 "init_toplevel"
380 "kill"
381 "kill_thy"
382 "linear_undo"
383 "pretty_setmargin"
384 "quit"
385 "remove_thy"
386 "undo"
387 "undos_proof"
388 "use_thy"))
390 (defconst isar-keywords-diag
391 '("ML_command"
392 "ML_val"
393 "approximate"
394 "cartouche"
395 "class_deps"
396 "code_deps"
397 "code_thms"
398 "display_drafts"
399 "find_consts"
400 "find_theorems"
401 "find_unused_assms"
402 "full_prf"
403 "header"
404 "help"
405 "locale_deps"
406 "nitpick"
407 "pr"
408 "prf"
409 "print_ML_antiquotations"
410 "print_abbrevs"
411 "print_antiquotations"
412 "print_attributes"
413 "print_binds"
414 "print_bnfs"
415 "print_bundles"
416 "print_case_translations"
417 "print_cases"
418 "print_claset"
419 "print_classes"
420 "print_codeproc"
421 "print_codesetup"
422 "print_coercions"
423 "print_commands"
424 "print_context"
425 "print_defn_rules"
426 "print_dependencies"
427 "print_facts"
428 "print_induct_rules"
429 "print_inductives"
430 "print_interps"
431 "print_locale"
432 "print_locales"
433 "print_methods"
434 "print_options"
435 "print_orders"
436 "print_quot_maps"
437 "print_quotconsts"
438 "print_quotients"
439 "print_quotientsQ3"
440 "print_quotmapsQ3"
441 "print_rules"
442 "print_simpset"
443 "print_state"
444 "print_statement"
445 "print_syntax"
446 "print_term_bindings"
447 "print_theorems"
448 "print_theory"
449 "print_trans_rules"
450 "prop"
451 "quickcheck"
452 "refute"
453 "sledgehammer"
454 "smt2_status"
455 "smt_status"
456 "solve_direct"
457 "spark_status"
458 "term"
459 "term_cartouche"
460 "thm"
461 "thm_deps"
462 "thy_deps"
463 "try"
464 "try0"
465 "typ"
466 "unused_thms"
467 "value"
468 "values"
469 "values_prolog"
470 "welcome"))
472 (defconst isar-keywords-theory-begin
473 '("theory"))
475 (defconst isar-keywords-theory-switch
476 '())
478 (defconst isar-keywords-theory-end
479 '("end"))
481 (defconst isar-keywords-theory-heading
482 '("chapter"
483 "section"
484 "subsection"
485 "subsubsection"))
487 (defconst isar-keywords-theory-decl
488 '("ML"
489 "ML_file"
490 "SML_export"
491 "SML_file"
492 "SML_import"
493 "abbreviation"
494 "adhoc_overloading"
495 "atom_decl"
496 "attribute_setup"
497 "axiomatization"
498 "bnf_axiomatization"
499 "boogie_file"
500 "bundle"
501 "case_of_simps"
502 "class"
503 "codatatype"
504 "code_datatype"
505 "code_identifier"
506 "code_monad"
507 "code_printing"
508 "code_reflect"
509 "code_reserved"
510 "coinductive"
511 "coinductive_set"
512 "consts"
513 "context"
514 "datatype"
515 "datatype_compat"
516 "datatype_new"
517 "declaration"
518 "declare"
519 "default_sort"
520 "defer_recdef"
521 "definition"
522 "defs"
523 "domain"
524 "domain_isomorphism"
525 "domaindef"
526 "equivariance"
527 "export_code"
528 "extract"
529 "extract_type"
530 "fixrec"
531 "fun"
532 "fun_cases"
533 "hide_class"
534 "hide_const"
535 "hide_fact"
536 "hide_type"
537 "import_const_map"
538 "import_file"
539 "import_tptp"
540 "import_type_map"
541 "inductive"
542 "inductive_cases"
543 "inductive_set"
544 "inductive_simps"
545 "instantiation"
546 "judgment"
547 "lemmas"
548 "lifting_forget"
549 "lifting_update"
550 "local_setup"
551 "locale"
552 "method_setup"
553 "nitpick_params"
554 "no_adhoc_overloading"
555 "no_notation"
556 "no_syntax"
557 "no_translations"
558 "no_type_notation"
559 "nominal_datatype"
560 "nonterminal"
561 "notation"
562 "notepad"
563 "oracle"
564 "overloading"
565 "parse_ast_translation"
566 "parse_translation"
567 "partial_function"
568 "primcorec"
569 "primrec"
570 "print_ast_translation"
571 "print_translation"
572 "quickcheck_generator"
573 "quickcheck_params"
574 "realizability"
575 "realizers"
576 "recdef"
577 "record"
578 "refute_params"
579 "setup"
580 "setup_lifting"
581 "simproc_setup"
582 "simps_of_case"
583 "sledgehammer_params"
584 "spark_end"
585 "spark_open"
586 "spark_open_vcg"
587 "spark_proof_functions"
588 "spark_types"
589 "statespace"
590 "syntax"
591 "syntax_declaration"
592 "text"
593 "text_cartouche"
594 "text_raw"
595 "theorems"
596 "translations"
597 "type_notation"
598 "type_synonym"
599 "typed_print_translation"
600 "typedecl"))
602 (defconst isar-keywords-theory-script
603 '())
605 (defconst isar-keywords-theory-goal
606 '("bnf"
607 "code_pred"
608 "corollary"
609 "cpodef"
610 "free_constructors"
611 "function"
612 "functor"
613 "instance"
614 "interpretation"
615 "lemma"
616 "lift_definition"
617 "nominal_function"
618 "nominal_inductive"
619 "nominal_inductive2"
620 "nominal_primrec"
621 "nominal_termination"
622 "pcpodef"
623 "permanent_interpretation"
624 "primcorecursive"
625 "quotient_definition"
626 "quotient_type"
627 "recdef_tc"
628 "rep_datatype"
629 "schematic_corollary"
630 "schematic_lemma"
631 "schematic_theorem"
632 "spark_vc"
633 "specification"
634 "subclass"
635 "sublocale"
636 "termination"
637 "theorem"
638 "typedef"))
640 (defconst isar-keywords-qed
641 '("\\."
642 "\\.\\."
643 "by"
644 "done"
645 "sorry"))
647 (defconst isar-keywords-qed-block
648 '("qed"))
650 (defconst isar-keywords-qed-global
651 '("oops"))
653 (defconst isar-keywords-proof-heading
654 '("sect"
655 "subsect"
656 "subsubsect"))
658 (defconst isar-keywords-proof-goal
659 '("have"
660 "hence"
661 "interpret"))
663 (defconst isar-keywords-proof-block
664 '("next"
665 "proof"))
667 (defconst isar-keywords-proof-open
668 '("{"))
670 (defconst isar-keywords-proof-close
671 '("}"))
673 (defconst isar-keywords-proof-chain
674 '("finally"
675 "from"
676 "then"
677 "ultimately"
678 "with"))
680 (defconst isar-keywords-proof-decl
681 '("ML_prf"
682 "also"
683 "include"
684 "including"
685 "let"
686 "moreover"
687 "note"
688 "txt"
689 "txt_raw"
690 "unfolding"
691 "using"
692 "write"))
694 (defconst isar-keywords-proof-asm
695 '("assume"
696 "case"
697 "def"
698 "fix"
699 "presume"))
701 (defconst isar-keywords-proof-asm-goal
702 '("guess"
703 "obtain"
704 "show"
705 "thus"))
707 (defconst isar-keywords-proof-script
708 '("apply"
709 "apply_end"
710 "back"
711 "defer"
712 "prefer"))
714 (provide 'isar-keywords)