| author | wenzelm |
| Mon, 26 Apr 2010 21:45:08 +0200 | |
| changeset 36366 | 5ab0f8859f9f |
| parent 36321 | 58d4dc6000fc |
| child 36455 | 30f96b4b108b |
| permissions | -rw-r--r-- |
1 ;;
2 ;; Keyword classification tables for Isabelle/Isar.
3 ;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-SMT + HOL-Statespace.
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
5 ;;
7 (defconst isar-keywords-major
8 '("\\."
9 "\\.\\."
10 "Isabelle\\.command"
11 "Isar\\.begin_document"
12 "Isar\\.define_command"
13 "Isar\\.edit_document"
14 "Isar\\.end_document"
15 "ML"
16 "ML_command"
17 "ML_prf"
18 "ML_val"
19 "ProofGeneral\\.inform_file_processed"
20 "ProofGeneral\\.inform_file_retracted"
21 "ProofGeneral\\.kill_proof"
22 "ProofGeneral\\.pr"
23 "ProofGeneral\\.process_pgip"
24 "ProofGeneral\\.restart"
25 "ProofGeneral\\.undo"
26 "abbreviation"
27 "also"
28 "apply"
29 "apply_end"
30 "arities"
31 "assume"
32 "atom_decl"
33 "atp_info"
34 "atp_kill"
35 "atp_messages"
36 "atp_minimize"
37 "attribute_setup"
38 "automaton"
39 "ax_specification"
40 "axiomatization"
41 "axioms"
42 "back"
43 "boogie_end"
44 "boogie_open"
45 "boogie_status"
46 "boogie_vc"
47 "by"
48 "cannot_undo"
49 "case"
50 "cd"
51 "chapter"
52 "class"
53 "class_deps"
54 "classes"
55 "classrel"
56 "code_abort"
57 "code_class"
58 "code_const"
59 "code_datatype"
60 "code_deps"
61 "code_include"
62 "code_instance"
63 "code_library"
64 "code_module"
65 "code_modulename"
66 "code_monad"
67 "code_pred"
68 "code_reserved"
69 "code_thms"
70 "code_type"
71 "coinductive"
72 "coinductive_set"
73 "commit"
74 "constdefs"
75 "consts"
76 "consts_code"
77 "context"
78 "corollary"
79 "cpodef"
80 "datatype"
81 "declaration"
82 "declare"
83 "def"
84 "defaultsort"
85 "defer"
86 "defer_recdef"
87 "definition"
88 "defs"
89 "disable_pr"
90 "display_drafts"
91 "domain"
92 "domain_isomorphism"
93 "done"
94 "enable_pr"
95 "end"
96 "equivariance"
97 "example_proof"
98 "exit"
99 "export_code"
100 "extract"
101 "extract_type"
102 "finalconsts"
103 "finally"
104 "find_consts"
105 "find_theorems"
106 "fix"
107 "fixpat"
108 "fixrec"
109 "from"
110 "full_prf"
111 "fun"
112 "function"
113 "global"
114 "guess"
115 "have"
116 "header"
117 "help"
118 "hence"
119 "hide_class"
120 "hide_const"
121 "hide_fact"
122 "hide_type"
123 "inductive"
124 "inductive_cases"
125 "inductive_set"
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 "linear_undo"
138 "local"
139 "local_setup"
140 "locale"
141 "method_setup"
142 "moreover"
143 "new_domain"
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 "nonterminals"
156 "normal_form"
157 "notation"
158 "note"
159 "obtain"
160 "oops"
161 "oracle"
162 "overloading"
163 "parse_ast_translation"
164 "parse_translation"
165 "pcpodef"
166 "pr"
167 "prefer"
168 "presume"
169 "pretty_setmargin"
170 "prf"
171 "primrec"
172 "print_abbrevs"
173 "print_antiquotations"
174 "print_ast_translation"
175 "print_atps"
176 "print_attributes"
177 "print_binds"
178 "print_cases"
179 "print_claset"
180 "print_classes"
181 "print_codeproc"
182 "print_codesetup"
183 "print_commands"
184 "print_configs"
185 "print_context"
186 "print_drafts"
187 "print_facts"
188 "print_induct_rules"
189 "print_interps"
190 "print_locale"
191 "print_locales"
192 "print_methods"
193 "print_orders"
194 "print_quotconsts"
195 "print_quotients"
196 "print_quotmaps"
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_params"
211 "quit"
212 "quotient_definition"
213 "quotient_type"
214 "realizability"
215 "realizers"
216 "recdef"
217 "recdef_tc"
218 "record"
219 "refute"
220 "refute_params"
221 "remove_thy"
222 "rep_datatype"
223 "repdef"
224 "schematic_corollary"
225 "schematic_lemma"
226 "schematic_theorem"
227 "sect"
228 "section"
229 "setup"
230 "show"
231 "simproc_setup"
232 "sledgehammer"
233 "sledgehammer_params"
234 "smt_status"
235 "sorry"
236 "specification"
237 "statespace"
238 "subclass"
239 "sublocale"
240 "subsect"
241 "subsection"
242 "subsubsect"
243 "subsubsection"
244 "syntax"
245 "term"
246 "termination"
247 "text"
248 "text_raw"
249 "then"
250 "theorem"
251 "theorems"
252 "theory"
253 "thm"
254 "thm_deps"
255 "thus"
256 "thy_deps"
257 "touch_thy"
258 "translations"
259 "txt"
260 "txt_raw"
261 "typ"
262 "type_notation"
263 "typed_print_translation"
264 "typedecl"
265 "typedef"
266 "types"
267 "types_code"
268 "ultimately"
269 "undo"
270 "undos_proof"
271 "unfolding"
272 "unused_thms"
273 "use"
274 "use_thy"
275 "using"
276 "value"
277 "values"
278 "welcome"
279 "with"
280 "{"
281 "}"))
283 (defconst isar-keywords-minor
284 '("actions"
285 "advanced"
286 "and"
287 "assumes"
288 "attach"
289 "avoids"
290 "begin"
291 "binder"
292 "compose"
293 "congs"
294 "constrains"
295 "contains"
296 "defines"
297 "file"
298 "fixes"
299 "for"
300 "hide_action"
301 "hints"
302 "identifier"
303 "if"
304 "imports"
305 "in"
306 "infix"
307 "infixl"
308 "infixr"
309 "initially"
310 "inputs"
311 "internals"
312 "is"
313 "lazy"
314 "module_name"
315 "monos"
316 "morphisms"
317 "notes"
318 "obtains"
319 "open"
320 "output"
321 "outputs"
322 "overloaded"
323 "permissive"
324 "pervasive"
325 "post"
326 "pre"
327 "rename"
328 "restrict"
329 "shows"
330 "signature"
331 "states"
332 "structure"
333 "to"
334 "transitions"
335 "transrel"
336 "unchecked"
337 "uses"
338 "where"))
340 (defconst isar-keywords-control
341 '("Isabelle\\.command"
342 "Isar\\.begin_document"
343 "Isar\\.define_command"
344 "Isar\\.edit_document"
345 "Isar\\.end_document"
346 "ProofGeneral\\.inform_file_processed"
347 "ProofGeneral\\.inform_file_retracted"
348 "ProofGeneral\\.kill_proof"
349 "ProofGeneral\\.process_pgip"
350 "ProofGeneral\\.restart"
351 "ProofGeneral\\.undo"
352 "cannot_undo"
353 "exit"
354 "init_toplevel"
355 "kill"
356 "linear_undo"
357 "quit"
358 "undo"
359 "undos_proof"))
361 (defconst isar-keywords-diag
362 '("ML_command"
363 "ML_val"
364 "ProofGeneral\\.pr"
365 "atp_info"
366 "atp_kill"
367 "atp_messages"
368 "atp_minimize"
369 "boogie_status"
370 "cd"
371 "class_deps"
372 "code_deps"
373 "code_thms"
374 "commit"
375 "disable_pr"
376 "display_drafts"
377 "enable_pr"
378 "export_code"
379 "find_consts"
380 "find_theorems"
381 "full_prf"
382 "header"
383 "help"
384 "kill_thy"
385 "nitpick"
386 "normal_form"
387 "pr"
388 "pretty_setmargin"
389 "prf"
390 "print_abbrevs"
391 "print_antiquotations"
392 "print_atps"
393 "print_attributes"
394 "print_binds"
395 "print_cases"
396 "print_claset"
397 "print_classes"
398 "print_codeproc"
399 "print_codesetup"
400 "print_commands"
401 "print_configs"
402 "print_context"
403 "print_drafts"
404 "print_facts"
405 "print_induct_rules"
406 "print_interps"
407 "print_locale"
408 "print_locales"
409 "print_methods"
410 "print_orders"
411 "print_quotconsts"
412 "print_quotients"
413 "print_quotmaps"
414 "print_rules"
415 "print_simpset"
416 "print_statement"
417 "print_syntax"
418 "print_theorems"
419 "print_theory"
420 "print_trans_rules"
421 "prop"
422 "pwd"
423 "quickcheck"
424 "refute"
425 "remove_thy"
426 "sledgehammer"
427 "smt_status"
428 "term"
429 "thm"
430 "thm_deps"
431 "thy_deps"
432 "touch_thy"
433 "typ"
434 "unused_thms"
435 "use_thy"
436 "value"
437 "values"
438 "welcome"))
440 (defconst isar-keywords-theory-begin
441 '("theory"))
443 (defconst isar-keywords-theory-switch
444 '())
446 (defconst isar-keywords-theory-end
447 '("end"))
449 (defconst isar-keywords-theory-heading
450 '("chapter"
451 "section"
452 "subsection"
453 "subsubsection"))
455 (defconst isar-keywords-theory-decl
456 '("ML"
457 "abbreviation"
458 "arities"
459 "atom_decl"
460 "attribute_setup"
461 "automaton"
462 "axiomatization"
463 "axioms"
464 "boogie_end"
465 "boogie_open"
466 "class"
467 "classes"
468 "classrel"
469 "code_abort"
470 "code_class"
471 "code_const"
472 "code_datatype"
473 "code_include"
474 "code_instance"
475 "code_library"
476 "code_module"
477 "code_modulename"
478 "code_monad"
479 "code_reserved"
480 "code_type"
481 "coinductive"
482 "coinductive_set"
483 "constdefs"
484 "consts"
485 "consts_code"
486 "context"
487 "datatype"
488 "declaration"
489 "declare"
490 "defaultsort"
491 "defer_recdef"
492 "definition"
493 "defs"
494 "domain"
495 "domain_isomorphism"
496 "equivariance"
497 "extract"
498 "extract_type"
499 "finalconsts"
500 "fixpat"
501 "fixrec"
502 "fun"
503 "global"
504 "hide_class"
505 "hide_const"
506 "hide_fact"
507 "hide_type"
508 "inductive"
509 "inductive_set"
510 "instantiation"
511 "judgment"
512 "lemmas"
513 "local"
514 "local_setup"
515 "locale"
516 "method_setup"
517 "new_domain"
518 "nitpick_params"
519 "no_notation"
520 "no_syntax"
521 "no_translations"
522 "no_type_notation"
523 "nominal_datatype"
524 "nonterminals"
525 "notation"
526 "oracle"
527 "overloading"
528 "parse_ast_translation"
529 "parse_translation"
530 "primrec"
531 "print_ast_translation"
532 "print_translation"
533 "quickcheck_params"
534 "quotient_definition"
535 "realizability"
536 "realizers"
537 "recdef"
538 "record"
539 "refute_params"
540 "repdef"
541 "setup"
542 "simproc_setup"
543 "sledgehammer_params"
544 "statespace"
545 "syntax"
546 "text"
547 "text_raw"
548 "theorems"
549 "translations"
550 "type_notation"
551 "typed_print_translation"
552 "typedecl"
553 "types"
554 "types_code"
555 "use"))
557 (defconst isar-keywords-theory-script
558 '("inductive_cases"))
560 (defconst isar-keywords-theory-goal
561 '("ax_specification"
562 "boogie_vc"
563 "code_pred"
564 "corollary"
565 "cpodef"
566 "example_proof"
567 "function"
568 "instance"
569 "interpretation"
570 "lemma"
571 "nominal_inductive"
572 "nominal_inductive2"
573 "nominal_primrec"
574 "pcpodef"
575 "quotient_type"
576 "recdef_tc"
577 "rep_datatype"
578 "schematic_corollary"
579 "schematic_lemma"
580 "schematic_theorem"
581 "specification"
582 "subclass"
583 "sublocale"
584 "termination"
585 "theorem"
586 "typedef"))
588 (defconst isar-keywords-qed
589 '("\\."
590 "\\.\\."
591 "by"
592 "done"
593 "sorry"))
595 (defconst isar-keywords-qed-block
596 '("qed"))
598 (defconst isar-keywords-qed-global
599 '("oops"))
601 (defconst isar-keywords-proof-heading
602 '("sect"
603 "subsect"
604 "subsubsect"))
606 (defconst isar-keywords-proof-goal
607 '("have"
608 "hence"
609 "interpret"))
611 (defconst isar-keywords-proof-block
612 '("next"
613 "proof"))
615 (defconst isar-keywords-proof-open
616 '("{"))
618 (defconst isar-keywords-proof-close
619 '("}"))
621 (defconst isar-keywords-proof-chain
622 '("finally"
623 "from"
624 "then"
625 "ultimately"
626 "with"))
628 (defconst isar-keywords-proof-decl
629 '("ML_prf"
630 "also"
631 "let"
632 "moreover"
633 "note"
634 "txt"
635 "txt_raw"
636 "unfolding"
637 "using"))
639 (defconst isar-keywords-proof-asm
640 '("assume"
641 "case"
642 "def"
643 "fix"
644 "presume"))
646 (defconst isar-keywords-proof-asm-goal
647 '("guess"
648 "obtain"
649 "show"
650 "thus"))
652 (defconst isar-keywords-proof-script
653 '("apply"
654 "apply_end"
655 "back"
656 "defer"
657 "prefer"))
659 (provide 'isar-keywords)