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