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