author | haftmann |
Sun, 11 Apr 2010 17:40:43 +0200 | |
changeset 36114 | e49fd7b1d932 |
parent 35419 | cc8e4276d093 |
child 36180 | 2db3711b2b03 |
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 "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 "no_type_notation"
147 "nominal_datatype"
148 "nominal_inductive"
149 "nominal_inductive2"
150 "nominal_primrec"
151 "nonterminals"
152 "normal_form"
153 "notation"
154 "note"
155 "obtain"
156 "oops"
157 "oracle"
158 "overloading"
159 "parse_ast_translation"
160 "parse_translation"
161 "pcpodef"
162 "pr"
163 "prefer"
164 "presume"
165 "pretty_setmargin"
166 "prf"
167 "primrec"
168 "print_abbrevs"
169 "print_antiquotations"
170 "print_ast_translation"
171 "print_atps"
172 "print_attributes"
173 "print_binds"
174 "print_cases"
175 "print_claset"
176 "print_classes"
177 "print_codeproc"
178 "print_codesetup"
179 "print_commands"
180 "print_configs"
181 "print_context"
182 "print_drafts"
183 "print_facts"
184 "print_induct_rules"
185 "print_interps"
186 "print_locale"
187 "print_locales"
188 "print_methods"
189 "print_orders"
190 "print_quotconsts"
191 "print_quotients"
192 "print_quotmaps"
193 "print_rules"
194 "print_simpset"
195 "print_statement"
196 "print_syntax"
197 "print_theorems"
198 "print_theory"
199 "print_trans_rules"
200 "print_translation"
201 "proof"
202 "prop"
203 "pwd"
204 "qed"
205 "quickcheck"
206 "quickcheck_params"
207 "quit"
208 "quotient_definition"
209 "quotient_type"
210 "realizability"
211 "realizers"
212 "recdef"
213 "recdef_tc"
214 "record"
215 "refute"
216 "refute_params"
217 "remove_thy"
218 "rep_datatype"
219 "repdef"
220 "sect"
221 "section"
222 "setup"
223 "show"
224 "simproc_setup"
225 "sledgehammer"
226 "sledgehammer_params"
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 "sledgehammer_params"
534 "statespace"
535 "syntax"
536 "text"
537 "text_raw"
538 "theorems"
539 "translations"
540 "type_notation"
541 "typed_print_translation"
542 "typedecl"
543 "types"
544 "types_code"
545 "use"))
547 (defconst isar-keywords-theory-script
548 '("inductive_cases"))
550 (defconst isar-keywords-theory-goal
551 '("ax_specification"
552 "boogie_vc"
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)