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