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