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