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