| author | wenzelm |
| Sat, 21 Nov 2009 20:41:29 +0100 | |
| changeset 33840 | f00a8956d6d0 |
| parent 33687 | 3222fa052846 |
| child 33874 | 1db5ca5eadf5 |
| 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-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\\.process_pgip"
23 "ProofGeneral\\.restart"
24 "ProofGeneral\\.undo"
25 "abbreviation"
26 "also"
27 "apply"
28 "apply_end"
29 "arities"
30 "assume"
31 "atom_decl"
32 "atp_info"
33 "atp_kill"
34 "atp_messages"
35 "atp_minimize"
36 "attribute_setup"
37 "automaton"
38 "ax_specification"
39 "axclass"
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 "exit"
98 "export_code"
99 "extract"
100 "extract_type"
101 "finalconsts"
102 "finally"
103 "find_consts"
104 "find_theorems"
105 "fix"
106 "fixpat"
107 "fixrec"
108 "from"
109 "full_prf"
110 "fun"
111 "function"
112 "global"
113 "guess"
114 "have"
115 "header"
116 "help"
117 "hence"
118 "hide"
119 "inductive"
120 "inductive_cases"
121 "inductive_set"
122 "init_toplevel"
123 "instance"
124 "instantiation"
125 "interpret"
126 "interpretation"
127 "judgment"
128 "kill"
129 "kill_thy"
130 "lemma"
131 "lemmas"
132 "let"
133 "linear_undo"
134 "local"
135 "local_setup"
136 "locale"
137 "method_setup"
138 "moreover"
139 "new_domain"
140 "next"
141 "nitpick"
142 "nitpick_params"
143 "no_notation"
144 "no_syntax"
145 "no_translations"
146 "nominal_datatype"
147 "nominal_inductive"
148 "nominal_inductive2"
149 "nominal_primrec"
150 "nonterminals"
151 "normal_form"
152 "notation"
153 "note"
154 "obtain"
155 "oops"
156 "oracle"
157 "overloading"
158 "parse_ast_translation"
159 "parse_translation"
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_atps"
171 "print_attributes"
172 "print_binds"
173 "print_cases"
174 "print_claset"
175 "print_classes"
176 "print_codeproc"
177 "print_codesetup"
178 "print_commands"
179 "print_configs"
180 "print_context"
181 "print_drafts"
182 "print_facts"
183 "print_induct_rules"
184 "print_interps"
185 "print_locale"
186 "print_locales"
187 "print_methods"
188 "print_orders"
189 "print_rules"
190 "print_simpset"
191 "print_statement"
192 "print_syntax"
193 "print_theorems"
194 "print_theory"
195 "print_trans_rules"
196 "print_translation"
197 "proof"
198 "prop"
199 "pwd"
200 "qed"
201 "quickcheck"
202 "quickcheck_params"
203 "quit"
204 "realizability"
205 "realizers"
206 "recdef"
207 "recdef_tc"
208 "record"
209 "refute"
210 "refute_params"
211 "remove_thy"
212 "rep_datatype"
213 "repdef"
214 "sect"
215 "section"
216 "setup"
217 "show"
218 "simproc_setup"
219 "sledgehammer"
220 "sorry"
221 "specification"
222 "statespace"
223 "subclass"
224 "sublocale"
225 "subsect"
226 "subsection"
227 "subsubsect"
228 "subsubsection"
229 "syntax"
230 "term"
231 "termination"
232 "text"
233 "text_raw"
234 "then"
235 "theorem"
236 "theorems"
237 "theory"
238 "thm"
239 "thm_deps"
240 "thus"
241 "thy_deps"
242 "touch_thy"
243 "translations"
244 "txt"
245 "txt_raw"
246 "typ"
247 "typed_print_translation"
248 "typedecl"
249 "typedef"
250 "types"
251 "types_code"
252 "ultimately"
253 "undo"
254 "undos_proof"
255 "unfolding"
256 "unused_thms"
257 "use"
258 "use_thy"
259 "using"
260 "value"
261 "values"
262 "welcome"
263 "with"
264 "{"
265 "}"))
267 (defconst isar-keywords-minor
268 '("actions"
269 "advanced"
270 "and"
271 "assumes"
272 "attach"
273 "avoids"
274 "begin"
275 "binder"
276 "compose"
277 "congs"
278 "constrains"
279 "contains"
280 "defines"
281 "file"
282 "fixes"
283 "for"
284 "hide_action"
285 "hints"
286 "identifier"
287 "if"
288 "imports"
289 "in"
290 "infix"
291 "infixl"
292 "infixr"
293 "initially"
294 "inputs"
295 "internals"
296 "is"
297 "lazy"
298 "module_name"
299 "monos"
300 "morphisms"
301 "notes"
302 "obtains"
303 "open"
304 "output"
305 "outputs"
306 "overloaded"
307 "permissive"
308 "pervasive"
309 "post"
310 "pre"
311 "rename"
312 "restrict"
313 "shows"
314 "signature"
315 "states"
316 "structure"
317 "to"
318 "transitions"
319 "transrel"
320 "unchecked"
321 "uses"
322 "where"))
324 (defconst isar-keywords-control
325 '("Isabelle\\.command"
326 "Isar\\.begin_document"
327 "Isar\\.define_command"
328 "Isar\\.edit_document"
329 "Isar\\.end_document"
330 "ProofGeneral\\.inform_file_processed"
331 "ProofGeneral\\.inform_file_retracted"
332 "ProofGeneral\\.kill_proof"
333 "ProofGeneral\\.process_pgip"
334 "ProofGeneral\\.restart"
335 "ProofGeneral\\.undo"
336 "cannot_undo"
337 "exit"
338 "init_toplevel"
339 "kill"
340 "linear_undo"
341 "quit"
342 "undo"
343 "undos_proof"))
345 (defconst isar-keywords-diag
346 '("ML_command"
347 "ML_val"
348 "atp_info"
349 "atp_kill"
350 "atp_messages"
351 "atp_minimize"
352 "boogie_status"
353 "cd"
354 "class_deps"
355 "code_deps"
356 "code_thms"
357 "commit"
358 "disable_pr"
359 "display_drafts"
360 "enable_pr"
361 "export_code"
362 "find_consts"
363 "find_theorems"
364 "full_prf"
365 "header"
366 "help"
367 "kill_thy"
368 "nitpick"
369 "normal_form"
370 "pr"
371 "pretty_setmargin"
372 "prf"
373 "print_abbrevs"
374 "print_antiquotations"
375 "print_atps"
376 "print_attributes"
377 "print_binds"
378 "print_cases"
379 "print_claset"
380 "print_classes"
381 "print_codeproc"
382 "print_codesetup"
383 "print_commands"
384 "print_configs"
385 "print_context"
386 "print_drafts"
387 "print_facts"
388 "print_induct_rules"
389 "print_interps"
390 "print_locale"
391 "print_locales"
392 "print_methods"
393 "print_orders"
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 "remove_thy"
406 "sledgehammer"
407 "term"
408 "thm"
409 "thm_deps"
410 "thy_deps"
411 "touch_thy"
412 "typ"
413 "unused_thms"
414 "use_thy"
415 "value"
416 "values"
417 "welcome"))
419 (defconst isar-keywords-theory-begin
420 '("theory"))
422 (defconst isar-keywords-theory-switch
423 '())
425 (defconst isar-keywords-theory-end
426 '("end"))
428 (defconst isar-keywords-theory-heading
429 '("chapter"
430 "section"
431 "subsection"
432 "subsubsection"))
434 (defconst isar-keywords-theory-decl
435 '("ML"
436 "abbreviation"
437 "arities"
438 "atom_decl"
439 "attribute_setup"
440 "automaton"
441 "axclass"
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_library"
456 "code_module"
457 "code_modulename"
458 "code_monad"
459 "code_reserved"
460 "code_type"
461 "coinductive"
462 "coinductive_set"
463 "constdefs"
464 "consts"
465 "consts_code"
466 "context"
467 "datatype"
468 "declaration"
469 "declare"
470 "defaultsort"
471 "defer_recdef"
472 "definition"
473 "defs"
474 "domain"
475 "domain_isomorphism"
476 "equivariance"
477 "extract"
478 "extract_type"
479 "finalconsts"
480 "fixpat"
481 "fixrec"
482 "fun"
483 "global"
484 "hide"
485 "inductive"
486 "inductive_set"
487 "instantiation"
488 "judgment"
489 "lemmas"
490 "local"
491 "local_setup"
492 "locale"
493 "method_setup"
494 "new_domain"
495 "nitpick_params"
496 "no_notation"
497 "no_syntax"
498 "no_translations"
499 "nominal_datatype"
500 "nonterminals"
501 "notation"
502 "oracle"
503 "overloading"
504 "parse_ast_translation"
505 "parse_translation"
506 "primrec"
507 "print_ast_translation"
508 "print_translation"
509 "quickcheck_params"
510 "realizability"
511 "realizers"
512 "recdef"
513 "record"
514 "refute_params"
515 "repdef"
516 "setup"
517 "simproc_setup"
518 "statespace"
519 "syntax"
520 "text"
521 "text_raw"
522 "theorems"
523 "translations"
524 "typed_print_translation"
525 "typedecl"
526 "types"
527 "types_code"
528 "use"))
530 (defconst isar-keywords-theory-script
531 '("inductive_cases"))
533 (defconst isar-keywords-theory-goal
534 '("ax_specification"
535 "boogie_vc"
536 "code_pred"
537 "corollary"
538 "cpodef"
539 "function"
540 "instance"
541 "interpretation"
542 "lemma"
543 "nominal_inductive"
544 "nominal_inductive2"
545 "nominal_primrec"
546 "pcpodef"
547 "recdef_tc"
548 "rep_datatype"
549 "specification"
550 "subclass"
551 "sublocale"
552 "termination"
553 "theorem"
554 "typedef"))
556 (defconst isar-keywords-qed
557 '("\\."
558 "\\.\\."
559 "by"
560 "done"
561 "sorry"))
563 (defconst isar-keywords-qed-block
564 '("qed"))
566 (defconst isar-keywords-qed-global
567 '("oops"))
569 (defconst isar-keywords-proof-heading
570 '("sect"
571 "subsect"
572 "subsubsect"))
574 (defconst isar-keywords-proof-goal
575 '("have"
576 "hence"
577 "interpret"))
579 (defconst isar-keywords-proof-block
580 '("next"
581 "proof"))
583 (defconst isar-keywords-proof-open
584 '("{"))
586 (defconst isar-keywords-proof-close
587 '("}"))
589 (defconst isar-keywords-proof-chain
590 '("finally"
591 "from"
592 "then"
593 "ultimately"
594 "with"))
596 (defconst isar-keywords-proof-decl
597 '("ML_prf"
598 "also"
599 "let"
600 "moreover"
601 "note"
602 "txt"
603 "txt_raw"
604 "unfolding"
605 "using"))
607 (defconst isar-keywords-proof-asm
608 '("assume"
609 "case"
610 "def"
611 "fix"
612 "presume"))
614 (defconst isar-keywords-proof-asm-goal
615 '("guess"
616 "obtain"
617 "show"
618 "thus"))
620 (defconst isar-keywords-proof-script
621 '("apply"
622 "apply_end"
623 "back"
624 "defer"
625 "prefer"))
627 (provide 'isar-keywords)