| author | wenzelm |
| Mon, 15 Dec 2008 21:41:21 +0100 | |
| changeset 29113 | fb31b7a6c858 |
| parent 28895 | 4e2914c2f8c5 |
| child 29252 | ea97aa6aeba2 |
| permissions | -rw-r--r-- |
1 ;;
2 ;; Keyword classification tables for Isabelle/Isar.
3 ;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
5 ;;
6 ;; $Id$
7 ;;
9 (defconst isar-keywords-major
10 '("\\."
11 "\\.\\."
12 "Isabelle\\.command"
13 "Isar\\.command"
14 "Isar\\.insert"
15 "Isar\\.remove"
16 "ML"
17 "ML_command"
18 "ML_prf"
19 "ML_val"
20 "ProofGeneral\\.inform_file_processed"
21 "ProofGeneral\\.inform_file_retracted"
22 "ProofGeneral\\.kill_proof"
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 "automaton"
37 "ax_specification"
38 "axclass"
39 "axiomatization"
40 "axioms"
41 "back"
42 "by"
43 "cannot_undo"
44 "case"
45 "cd"
46 "chapter"
47 "class"
48 "class_deps"
49 "classes"
50 "classrel"
51 "code_abort"
52 "code_class"
53 "code_const"
54 "code_datatype"
55 "code_deps"
56 "code_include"
57 "code_instance"
58 "code_library"
59 "code_module"
60 "code_modulename"
61 "code_monad"
62 "code_reserved"
63 "code_thms"
64 "code_type"
65 "coinductive"
66 "coinductive_set"
67 "commit"
68 "constdefs"
69 "consts"
70 "consts_code"
71 "context"
72 "corollary"
73 "cpodef"
74 "datatype"
75 "declaration"
76 "declare"
77 "def"
78 "defaultsort"
79 "defer"
80 "defer_recdef"
81 "definition"
82 "defs"
83 "disable_pr"
84 "display_drafts"
85 "domain"
86 "done"
87 "enable_pr"
88 "end"
89 "equivariance"
90 "exit"
91 "export_code"
92 "extract"
93 "extract_type"
94 "finalconsts"
95 "finally"
96 "find_theorems"
97 "fix"
98 "fixpat"
99 "fixrec"
100 "from"
101 "full_prf"
102 "fun"
103 "function"
104 "global"
105 "guess"
106 "have"
107 "header"
108 "help"
109 "hence"
110 "hide"
111 "inductive"
112 "inductive_cases"
113 "inductive_set"
114 "init_toplevel"
115 "instance"
116 "instantiation"
117 "interpret"
118 "interpretation"
119 "invoke"
120 "judgment"
121 "kill"
122 "kill_thy"
123 "lemma"
124 "lemmas"
125 "let"
126 "linear_undo"
127 "local"
128 "locale"
129 "method_setup"
130 "moreover"
131 "next"
132 "no_notation"
133 "no_syntax"
134 "no_translations"
135 "nominal_datatype"
136 "nominal_inductive"
137 "nominal_inductive2"
138 "nominal_primrec"
139 "nonterminals"
140 "normal_form"
141 "notation"
142 "note"
143 "obtain"
144 "oops"
145 "oracle"
146 "overloading"
147 "parse_ast_translation"
148 "parse_translation"
149 "pcpodef"
150 "pr"
151 "prefer"
152 "presume"
153 "pretty_setmargin"
154 "prf"
155 "primrec"
156 "print_abbrevs"
157 "print_antiquotations"
158 "print_ast_translation"
159 "print_atps"
160 "print_attributes"
161 "print_binds"
162 "print_cases"
163 "print_claset"
164 "print_classes"
165 "print_codesetup"
166 "print_commands"
167 "print_configs"
168 "print_context"
169 "print_drafts"
170 "print_facts"
171 "print_induct_rules"
172 "print_interps"
173 "print_locale"
174 "print_locales"
175 "print_methods"
176 "print_orders"
177 "print_rules"
178 "print_simpset"
179 "print_statement"
180 "print_syntax"
181 "print_theorems"
182 "print_theory"
183 "print_trans_rules"
184 "print_translation"
185 "proof"
186 "prop"
187 "pwd"
188 "qed"
189 "quickcheck"
190 "quickcheck_params"
191 "quit"
192 "realizability"
193 "realizers"
194 "recdef"
195 "recdef_tc"
196 "record"
197 "refute"
198 "refute_params"
199 "remove_thy"
200 "rep_datatype"
201 "sect"
202 "section"
203 "setup"
204 "show"
205 "simproc_setup"
206 "sledgehammer"
207 "sorry"
208 "specification"
209 "statespace"
210 "subclass"
211 "sublocale"
212 "subsect"
213 "subsection"
214 "subsubsect"
215 "subsubsection"
216 "syntax"
217 "term"
218 "termination"
219 "text"
220 "text_raw"
221 "then"
222 "theorem"
223 "theorems"
224 "theory"
225 "thm"
226 "thm_deps"
227 "thus"
228 "thy_deps"
229 "touch_thy"
230 "translations"
231 "txt"
232 "txt_raw"
233 "typ"
234 "typed_print_translation"
235 "typedecl"
236 "typedef"
237 "types"
238 "types_code"
239 "ultimately"
240 "undo"
241 "undos_proof"
242 "unfolding"
243 "unused_thms"
244 "use"
245 "use_thy"
246 "using"
247 "value"
248 "welcome"
249 "with"
250 "{"
251 "}"))
253 (defconst isar-keywords-minor
254 '("actions"
255 "advanced"
256 "and"
257 "assumes"
258 "attach"
259 "avoids"
260 "begin"
261 "binder"
262 "compose"
263 "congs"
264 "constrains"
265 "contains"
266 "defines"
267 "file"
268 "fixes"
269 "for"
270 "hide_action"
271 "hints"
272 "identifier"
273 "if"
274 "imports"
275 "in"
276 "infix"
277 "infixl"
278 "infixr"
279 "initially"
280 "inputs"
281 "internals"
282 "is"
283 "lazy"
284 "module_name"
285 "monos"
286 "morphisms"
287 "notes"
288 "obtains"
289 "open"
290 "otherwise"
291 "output"
292 "outputs"
293 "overloaded"
294 "permissive"
295 "post"
296 "pre"
297 "rename"
298 "restrict"
299 "shows"
300 "signature"
301 "states"
302 "structure"
303 "to"
304 "transitions"
305 "transrel"
306 "unchecked"
307 "uses"
308 "where"))
310 (defconst isar-keywords-control
311 '("Isabelle\\.command"
312 "Isar\\.command"
313 "Isar\\.insert"
314 "Isar\\.remove"
315 "ProofGeneral\\.inform_file_processed"
316 "ProofGeneral\\.inform_file_retracted"
317 "ProofGeneral\\.kill_proof"
318 "ProofGeneral\\.process_pgip"
319 "ProofGeneral\\.restart"
320 "ProofGeneral\\.undo"
321 "cannot_undo"
322 "exit"
323 "init_toplevel"
324 "kill"
325 "linear_undo"
326 "quit"
327 "undo"
328 "undos_proof"))
330 (defconst isar-keywords-diag
331 '("ML_command"
332 "ML_val"
333 "atp_info"
334 "atp_kill"
335 "atp_messages"
336 "cd"
337 "class_deps"
338 "code_deps"
339 "code_thms"
340 "commit"
341 "disable_pr"
342 "display_drafts"
343 "enable_pr"
344 "export_code"
345 "find_theorems"
346 "full_prf"
347 "header"
348 "help"
349 "kill_thy"
350 "normal_form"
351 "pr"
352 "pretty_setmargin"
353 "prf"
354 "print_abbrevs"
355 "print_antiquotations"
356 "print_atps"
357 "print_attributes"
358 "print_binds"
359 "print_cases"
360 "print_claset"
361 "print_classes"
362 "print_codesetup"
363 "print_commands"
364 "print_configs"
365 "print_context"
366 "print_drafts"
367 "print_facts"
368 "print_induct_rules"
369 "print_interps"
370 "print_locale"
371 "print_locales"
372 "print_methods"
373 "print_orders"
374 "print_rules"
375 "print_simpset"
376 "print_statement"
377 "print_syntax"
378 "print_theorems"
379 "print_theory"
380 "print_trans_rules"
381 "prop"
382 "pwd"
383 "quickcheck"
384 "refute"
385 "remove_thy"
386 "sledgehammer"
387 "term"
388 "thm"
389 "thm_deps"
390 "thy_deps"
391 "touch_thy"
392 "typ"
393 "unused_thms"
394 "use_thy"
395 "value"
396 "welcome"))
398 (defconst isar-keywords-theory-begin
399 '("theory"))
401 (defconst isar-keywords-theory-switch
402 '())
404 (defconst isar-keywords-theory-end
405 '("end"))
407 (defconst isar-keywords-theory-heading
408 '("chapter"
409 "section"
410 "subsection"
411 "subsubsection"))
413 (defconst isar-keywords-theory-decl
414 '("ML"
415 "abbreviation"
416 "arities"
417 "atom_decl"
418 "automaton"
419 "axclass"
420 "axiomatization"
421 "axioms"
422 "class"
423 "classes"
424 "classrel"
425 "code_abort"
426 "code_class"
427 "code_const"
428 "code_datatype"
429 "code_include"
430 "code_instance"
431 "code_library"
432 "code_module"
433 "code_modulename"
434 "code_monad"
435 "code_reserved"
436 "code_type"
437 "coinductive"
438 "coinductive_set"
439 "constdefs"
440 "consts"
441 "consts_code"
442 "context"
443 "datatype"
444 "declaration"
445 "declare"
446 "defaultsort"
447 "defer_recdef"
448 "definition"
449 "defs"
450 "domain"
451 "equivariance"
452 "extract"
453 "extract_type"
454 "finalconsts"
455 "fixpat"
456 "fixrec"
457 "fun"
458 "global"
459 "hide"
460 "inductive"
461 "inductive_set"
462 "instantiation"
463 "judgment"
464 "lemmas"
465 "local"
466 "locale"
467 "method_setup"
468 "no_notation"
469 "no_syntax"
470 "no_translations"
471 "nominal_datatype"
472 "nonterminals"
473 "notation"
474 "oracle"
475 "overloading"
476 "parse_ast_translation"
477 "parse_translation"
478 "primrec"
479 "print_ast_translation"
480 "print_translation"
481 "quickcheck_params"
482 "realizability"
483 "realizers"
484 "recdef"
485 "record"
486 "refute_params"
487 "setup"
488 "simproc_setup"
489 "statespace"
490 "syntax"
491 "text"
492 "text_raw"
493 "theorems"
494 "translations"
495 "typed_print_translation"
496 "typedecl"
497 "types"
498 "types_code"
499 "use"))
501 (defconst isar-keywords-theory-script
502 '("inductive_cases"))
504 (defconst isar-keywords-theory-goal
505 '("ax_specification"
506 "corollary"
507 "cpodef"
508 "function"
509 "instance"
510 "interpretation"
511 "lemma"
512 "nominal_inductive"
513 "nominal_inductive2"
514 "nominal_primrec"
515 "pcpodef"
516 "recdef_tc"
517 "rep_datatype"
518 "specification"
519 "subclass"
520 "sublocale"
521 "termination"
522 "theorem"
523 "typedef"))
525 (defconst isar-keywords-qed
526 '("\\."
527 "\\.\\."
528 "by"
529 "done"
530 "sorry"))
532 (defconst isar-keywords-qed-block
533 '("qed"))
535 (defconst isar-keywords-qed-global
536 '("oops"))
538 (defconst isar-keywords-proof-heading
539 '("sect"
540 "subsect"
541 "subsubsect"))
543 (defconst isar-keywords-proof-goal
544 '("have"
545 "hence"
546 "interpret"
547 "invoke"))
549 (defconst isar-keywords-proof-block
550 '("next"
551 "proof"))
553 (defconst isar-keywords-proof-open
554 '("{"))
556 (defconst isar-keywords-proof-close
557 '("}"))
559 (defconst isar-keywords-proof-chain
560 '("finally"
561 "from"
562 "then"
563 "ultimately"
564 "with"))
566 (defconst isar-keywords-proof-decl
567 '("ML_prf"
568 "also"
569 "let"
570 "moreover"
571 "note"
572 "txt"
573 "txt_raw"
574 "unfolding"
575 "using"))
577 (defconst isar-keywords-proof-asm
578 '("assume"
579 "case"
580 "def"
581 "fix"
582 "presume"))
584 (defconst isar-keywords-proof-asm-goal
585 '("guess"
586 "obtain"
587 "show"
588 "thus"))
590 (defconst isar-keywords-proof-script
591 '("apply"
592 "apply_end"
593 "back"
594 "defer"
595 "prefer"))
597 (provide 'isar-keywords)