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