| author | wenzelm |
| Mon, 01 Mar 2010 17:12:43 +0100 | |
| changeset 35419 | cc8e4276d093 |
| parent 35279 | 4f6760122b2a |
| child 36114 | e49fd7b1d932 |
| 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_abstype"
58 "code_class"
59 "code_const"
60 "code_datatype"
61 "code_deps"
62 "code_include"
63 "code_instance"
64 "code_library"
65 "code_module"
66 "code_modulename"
67 "code_monad"
68 "code_pred"
69 "code_reserved"
70 "code_thms"
71 "code_type"
72 "coinductive"
73 "coinductive_set"
74 "commit"
75 "constdefs"
76 "consts"
77 "consts_code"
78 "context"
79 "corollary"
80 "cpodef"
81 "datatype"
82 "declaration"
83 "declare"
84 "def"
85 "defaultsort"
86 "defer"
87 "defer_recdef"
88 "definition"
89 "defs"
90 "disable_pr"
91 "display_drafts"
92 "domain"
93 "domain_isomorphism"
94 "done"
95 "enable_pr"
96 "end"
97 "equivariance"
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"
120 "inductive"
121 "inductive_cases"
122 "inductive_set"
123 "init_toplevel"
124 "instance"
125 "instantiation"
126 "interpret"
127 "interpretation"
128 "judgment"
129 "kill"
130 "kill_thy"
131 "lemma"
132 "lemmas"
133 "let"
134 "linear_undo"
135 "local"
136 "local_setup"
137 "locale"
138 "method_setup"
139 "moreover"
140 "new_domain"
141 "next"
142 "nitpick"
143 "nitpick_params"
144 "no_notation"
145 "no_syntax"
146 "no_translations"
147 "no_type_notation"
148 "nominal_datatype"
149 "nominal_inductive"
150 "nominal_inductive2"
151 "nominal_primrec"
152 "nonterminals"
153 "normal_form"
154 "notation"
155 "note"
156 "obtain"
157 "oops"
158 "oracle"
159 "overloading"
160 "parse_ast_translation"
161 "parse_translation"
162 "pcpodef"
163 "pr"
164 "prefer"
165 "presume"
166 "pretty_setmargin"
167 "prf"
168 "primrec"
169 "print_abbrevs"
170 "print_antiquotations"
171 "print_ast_translation"
172 "print_atps"
173 "print_attributes"
174 "print_binds"
175 "print_cases"
176 "print_claset"
177 "print_classes"
178 "print_codeproc"
179 "print_codesetup"
180 "print_commands"
181 "print_configs"
182 "print_context"
183 "print_drafts"
184 "print_facts"
185 "print_induct_rules"
186 "print_interps"
187 "print_locale"
188 "print_locales"
189 "print_methods"
190 "print_orders"
191 "print_quotconsts"
192 "print_quotients"
193 "print_quotmaps"
194 "print_rules"
195 "print_simpset"
196 "print_statement"
197 "print_syntax"
198 "print_theorems"
199 "print_theory"
200 "print_trans_rules"
201 "print_translation"
202 "proof"
203 "prop"
204 "pwd"
205 "qed"
206 "quickcheck"
207 "quickcheck_params"
208 "quit"
209 "quotient_definition"
210 "quotient_type"
211 "realizability"
212 "realizers"
213 "recdef"
214 "recdef_tc"
215 "record"
216 "refute"
217 "refute_params"
218 "remove_thy"
219 "rep_datatype"
220 "repdef"
221 "sect"
222 "section"
223 "setup"
224 "show"
225 "simproc_setup"
226 "sledgehammer"
227 "smt_status"
228 "sorry"
229 "specification"
230 "statespace"
231 "subclass"
232 "sublocale"
233 "subsect"
234 "subsection"
235 "subsubsect"
236 "subsubsection"
237 "syntax"
238 "term"
239 "termination"
240 "text"
241 "text_raw"
242 "then"
243 "theorem"
244 "theorems"
245 "theory"
246 "thm"
247 "thm_deps"
248 "thus"
249 "thy_deps"
250 "touch_thy"
251 "translations"
252 "txt"
253 "txt_raw"
254 "typ"
255 "type_notation"
256 "typed_print_translation"
257 "typedecl"
258 "typedef"
259 "types"
260 "types_code"
261 "ultimately"
262 "undo"
263 "undos_proof"
264 "unfolding"
265 "unused_thms"
266 "use"
267 "use_thy"
268 "using"
269 "value"
270 "values"
271 "welcome"
272 "with"
273 "{"
274 "}"))
276 (defconst isar-keywords-minor
277 '("actions"
278 "advanced"
279 "and"
280 "assumes"
281 "attach"
282 "avoids"
283 "begin"
284 "binder"
285 "compose"
286 "congs"
287 "constrains"
288 "contains"
289 "defines"
290 "file"
291 "fixes"
292 "for"
293 "hide_action"
294 "hints"
295 "identifier"
296 "if"
297 "imports"
298 "in"
299 "infix"
300 "infixl"
301 "infixr"
302 "initially"
303 "inputs"
304 "internals"
305 "is"
306 "lazy"
307 "module_name"
308 "monos"
309 "morphisms"
310 "notes"
311 "obtains"
312 "open"
313 "output"
314 "outputs"
315 "overloaded"
316 "permissive"
317 "pervasive"
318 "post"
319 "pre"
320 "rename"
321 "restrict"
322 "shows"
323 "signature"
324 "states"
325 "structure"
326 "to"
327 "transitions"
328 "transrel"
329 "unchecked"
330 "uses"
331 "where"))
333 (defconst isar-keywords-control
334 '("Isabelle\\.command"
335 "Isar\\.begin_document"
336 "Isar\\.define_command"
337 "Isar\\.edit_document"
338 "Isar\\.end_document"
339 "ProofGeneral\\.inform_file_processed"
340 "ProofGeneral\\.inform_file_retracted"
341 "ProofGeneral\\.kill_proof"
342 "ProofGeneral\\.process_pgip"
343 "ProofGeneral\\.restart"
344 "ProofGeneral\\.undo"
345 "cannot_undo"
346 "exit"
347 "init_toplevel"
348 "kill"
349 "linear_undo"
350 "quit"
351 "undo"
352 "undos_proof"))
354 (defconst isar-keywords-diag
355 '("ML_command"
356 "ML_val"
357 "ProofGeneral\\.pr"
358 "atp_info"
359 "atp_kill"
360 "atp_messages"
361 "atp_minimize"
362 "boogie_status"
363 "cd"
364 "class_deps"
365 "code_deps"
366 "code_thms"
367 "commit"
368 "disable_pr"
369 "display_drafts"
370 "enable_pr"
371 "export_code"
372 "find_consts"
373 "find_theorems"
374 "full_prf"
375 "header"
376 "help"
377 "kill_thy"
378 "nitpick"
379 "normal_form"
380 "pr"
381 "pretty_setmargin"
382 "prf"
383 "print_abbrevs"
384 "print_antiquotations"
385 "print_atps"
386 "print_attributes"
387 "print_binds"
388 "print_cases"
389 "print_claset"
390 "print_classes"
391 "print_codeproc"
392 "print_codesetup"
393 "print_commands"
394 "print_configs"
395 "print_context"
396 "print_drafts"
397 "print_facts"
398 "print_induct_rules"
399 "print_interps"
400 "print_locale"
401 "print_locales"
402 "print_methods"
403 "print_orders"
404 "print_quotconsts"
405 "print_quotients"
406 "print_quotmaps"
407 "print_rules"
408 "print_simpset"
409 "print_statement"
410 "print_syntax"
411 "print_theorems"
412 "print_theory"
413 "print_trans_rules"
414 "prop"
415 "pwd"
416 "quickcheck"
417 "refute"
418 "remove_thy"
419 "sledgehammer"
420 "smt_status"
421 "term"
422 "thm"
423 "thm_deps"
424 "thy_deps"
425 "touch_thy"
426 "typ"
427 "unused_thms"
428 "use_thy"
429 "value"
430 "values"
431 "welcome"))
433 (defconst isar-keywords-theory-begin
434 '("theory"))
436 (defconst isar-keywords-theory-switch
437 '())
439 (defconst isar-keywords-theory-end
440 '("end"))
442 (defconst isar-keywords-theory-heading
443 '("chapter"
444 "section"
445 "subsection"
446 "subsubsection"))
448 (defconst isar-keywords-theory-decl
449 '("ML"
450 "abbreviation"
451 "arities"
452 "atom_decl"
453 "attribute_setup"
454 "automaton"
455 "axiomatization"
456 "axioms"
457 "boogie_end"
458 "boogie_open"
459 "class"
460 "classes"
461 "classrel"
462 "code_abort"
463 "code_class"
464 "code_const"
465 "code_datatype"
466 "code_include"
467 "code_instance"
468 "code_library"
469 "code_module"
470 "code_modulename"
471 "code_monad"
472 "code_reserved"
473 "code_type"
474 "coinductive"
475 "coinductive_set"
476 "constdefs"
477 "consts"
478 "consts_code"
479 "context"
480 "datatype"
481 "declaration"
482 "declare"
483 "defaultsort"
484 "defer_recdef"
485 "definition"
486 "defs"
487 "domain"
488 "domain_isomorphism"
489 "equivariance"
490 "extract"
491 "extract_type"
492 "finalconsts"
493 "fixpat"
494 "fixrec"
495 "fun"
496 "global"
497 "hide"
498 "inductive"
499 "inductive_set"
500 "instantiation"
501 "judgment"
502 "lemmas"
503 "local"
504 "local_setup"
505 "locale"
506 "method_setup"
507 "new_domain"
508 "nitpick_params"
509 "no_notation"
510 "no_syntax"
511 "no_translations"
512 "no_type_notation"
513 "nominal_datatype"
514 "nonterminals"
515 "notation"
516 "oracle"
517 "overloading"
518 "parse_ast_translation"
519 "parse_translation"
520 "primrec"
521 "print_ast_translation"
522 "print_translation"
523 "quickcheck_params"
524 "quotient_definition"
525 "realizability"
526 "realizers"
527 "recdef"
528 "record"
529 "refute_params"
530 "repdef"
531 "setup"
532 "simproc_setup"
533 "statespace"
534 "syntax"
535 "text"
536 "text_raw"
537 "theorems"
538 "translations"
539 "type_notation"
540 "typed_print_translation"
541 "typedecl"
542 "types"
543 "types_code"
544 "use"))
546 (defconst isar-keywords-theory-script
547 '("inductive_cases"))
549 (defconst isar-keywords-theory-goal
550 '("ax_specification"
551 "boogie_vc"
552 "code_abstype"
553 "code_pred"
554 "corollary"
555 "cpodef"
556 "function"
557 "instance"
558 "interpretation"
559 "lemma"
560 "nominal_inductive"
561 "nominal_inductive2"
562 "nominal_primrec"
563 "pcpodef"
564 "quotient_type"
565 "recdef_tc"
566 "rep_datatype"
567 "specification"
568 "subclass"
569 "sublocale"
570 "termination"
571 "theorem"
572 "typedef"))
574 (defconst isar-keywords-qed
575 '("\\."
576 "\\.\\."
577 "by"
578 "done"
579 "sorry"))
581 (defconst isar-keywords-qed-block
582 '("qed"))
584 (defconst isar-keywords-qed-global
585 '("oops"))
587 (defconst isar-keywords-proof-heading
588 '("sect"
589 "subsect"
590 "subsubsect"))
592 (defconst isar-keywords-proof-goal
593 '("have"
594 "hence"
595 "interpret"))
597 (defconst isar-keywords-proof-block
598 '("next"
599 "proof"))
601 (defconst isar-keywords-proof-open
602 '("{"))
604 (defconst isar-keywords-proof-close
605 '("}"))
607 (defconst isar-keywords-proof-chain
608 '("finally"
609 "from"
610 "then"
611 "ultimately"
612 "with"))
614 (defconst isar-keywords-proof-decl
615 '("ML_prf"
616 "also"
617 "let"
618 "moreover"
619 "note"
620 "txt"
621 "txt_raw"
622 "unfolding"
623 "using"))
625 (defconst isar-keywords-proof-asm
626 '("assume"
627 "case"
628 "def"
629 "fix"
630 "presume"))
632 (defconst isar-keywords-proof-asm-goal
633 '("guess"
634 "obtain"
635 "show"
636 "thus"))
638 (defconst isar-keywords-proof-script
639 '("apply"
640 "apply_end"
641 "back"
642 "defer"
643 "prefer"))
645 (provide 'isar-keywords)