| author | wenzelm |
| Wed, 16 Jul 2008 16:39:11 +0200 | |
| changeset 27621 | d96bd54d7446 |
| parent 27590 | 26415966c708 |
| child 28280 | fd0485db7d5a |
| permissions | -rw-r--r-- |
1 ;;
2 ;; Keyword classification tables for Isabelle/Isar.
3 ;; Generated from Pure + Pure-ProofGeneral + HOL-Plain + 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_val"
19 "ProofGeneral\\.inform_file_processed"
20 "ProofGeneral\\.inform_file_retracted"
21 "ProofGeneral\\.kill_proof"
22 "ProofGeneral\\.process_pgip"
23 "ProofGeneral\\.restart"
24 "ProofGeneral\\.undo"
25 "abbreviation"
26 "also"
27 "apply"
28 "apply_end"
29 "arities"
30 "assume"
31 "atom_decl"
32 "automaton"
33 "ax_specification"
34 "axclass"
35 "axiomatization"
36 "axioms"
37 "back"
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_reserved"
59 "code_thms"
60 "code_type"
61 "coinductive"
62 "coinductive_set"
63 "commit"
64 "constdefs"
65 "consts"
66 "consts_code"
67 "context"
68 "corollary"
69 "cpodef"
70 "datatype"
71 "declaration"
72 "declare"
73 "def"
74 "defaultsort"
75 "defer"
76 "defer_recdef"
77 "definition"
78 "defs"
79 "disable_pr"
80 "display_drafts"
81 "domain"
82 "done"
83 "enable_pr"
84 "end"
85 "equivariance"
86 "exit"
87 "export_code"
88 "extract"
89 "extract_type"
90 "finalconsts"
91 "finally"
92 "find_theorems"
93 "fix"
94 "fixpat"
95 "fixrec"
96 "from"
97 "full_prf"
98 "fun"
99 "function"
100 "global"
101 "guess"
102 "have"
103 "header"
104 "help"
105 "hence"
106 "hide"
107 "inductive"
108 "inductive_cases"
109 "inductive_set"
110 "init_toplevel"
111 "instance"
112 "instantiation"
113 "interpret"
114 "interpretation"
115 "invoke"
116 "judgment"
117 "kill"
118 "kill_thy"
119 "lemma"
120 "lemmas"
121 "let"
122 "linear_undo"
123 "local"
124 "locale"
125 "method_setup"
126 "moreover"
127 "next"
128 "no_notation"
129 "no_syntax"
130 "no_translations"
131 "nominal_datatype"
132 "nominal_inductive"
133 "nominal_primrec"
134 "nonterminals"
135 "normal_form"
136 "notation"
137 "note"
138 "obtain"
139 "oops"
140 "oracle"
141 "overloading"
142 "parse_ast_translation"
143 "parse_translation"
144 "pcpodef"
145 "pr"
146 "prefer"
147 "presume"
148 "pretty_setmargin"
149 "prf"
150 "primrec"
151 "print_abbrevs"
152 "print_antiquotations"
153 "print_ast_translation"
154 "print_attributes"
155 "print_binds"
156 "print_cases"
157 "print_claset"
158 "print_classes"
159 "print_codesetup"
160 "print_commands"
161 "print_configs"
162 "print_context"
163 "print_drafts"
164 "print_facts"
165 "print_induct_rules"
166 "print_interps"
167 "print_locale"
168 "print_locales"
169 "print_methods"
170 "print_orders"
171 "print_rules"
172 "print_simpset"
173 "print_statement"
174 "print_syntax"
175 "print_theorems"
176 "print_theory"
177 "print_trans_rules"
178 "print_translation"
179 "proof"
180 "prop"
181 "pwd"
182 "qed"
183 "quickcheck"
184 "quickcheck_params"
185 "quit"
186 "realizability"
187 "realizers"
188 "recdef"
189 "recdef_tc"
190 "record"
191 "refute"
192 "refute_params"
193 "remove_thy"
194 "rep_datatype"
195 "sect"
196 "section"
197 "setup"
198 "show"
199 "simproc_setup"
200 "sledgehammer"
201 "sorry"
202 "specification"
203 "statespace"
204 "subclass"
205 "subsect"
206 "subsection"
207 "subsubsect"
208 "subsubsection"
209 "syntax"
210 "term"
211 "termination"
212 "text"
213 "text_raw"
214 "then"
215 "theorem"
216 "theorems"
217 "theory"
218 "thm"
219 "thm_deps"
220 "thus"
221 "thy_deps"
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 "Isar\\.command"
307 "Isar\\.insert"
308 "Isar\\.remove"
309 "ProofGeneral\\.inform_file_processed"
310 "ProofGeneral\\.inform_file_retracted"
311 "ProofGeneral\\.kill_proof"
312 "ProofGeneral\\.process_pgip"
313 "ProofGeneral\\.restart"
314 "ProofGeneral\\.undo"
315 "cannot_undo"
316 "exit"
317 "init_toplevel"
318 "kill"
319 "linear_undo"
320 "quit"
321 "undo"
322 "undos_proof"))
324 (defconst isar-keywords-diag
325 '("ML_command"
326 "ML_val"
327 "cd"
328 "class_deps"
329 "code_deps"
330 "code_thms"
331 "commit"
332 "disable_pr"
333 "display_drafts"
334 "enable_pr"
335 "export_code"
336 "find_theorems"
337 "full_prf"
338 "header"
339 "help"
340 "kill_thy"
341 "normal_form"
342 "pr"
343 "pretty_setmargin"
344 "prf"
345 "print_abbrevs"
346 "print_antiquotations"
347 "print_attributes"
348 "print_binds"
349 "print_cases"
350 "print_claset"
351 "print_classes"
352 "print_codesetup"
353 "print_commands"
354 "print_configs"
355 "print_context"
356 "print_drafts"
357 "print_facts"
358 "print_induct_rules"
359 "print_interps"
360 "print_locale"
361 "print_locales"
362 "print_methods"
363 "print_orders"
364 "print_rules"
365 "print_simpset"
366 "print_statement"
367 "print_syntax"
368 "print_theorems"
369 "print_theory"
370 "print_trans_rules"
371 "prop"
372 "pwd"
373 "quickcheck"
374 "refute"
375 "remove_thy"
376 "sledgehammer"
377 "term"
378 "thm"
379 "thm_deps"
380 "thy_deps"
381 "touch_thy"
382 "typ"
383 "unused_thms"
384 "use_thy"
385 "value"
386 "welcome"))
388 (defconst isar-keywords-theory-begin
389 '("theory"))
391 (defconst isar-keywords-theory-switch
392 '())
394 (defconst isar-keywords-theory-end
395 '("end"))
397 (defconst isar-keywords-theory-heading
398 '("chapter"
399 "section"
400 "subsection"
401 "subsubsection"))
403 (defconst isar-keywords-theory-decl
404 '("ML"
405 "abbreviation"
406 "arities"
407 "atom_decl"
408 "automaton"
409 "axclass"
410 "axiomatization"
411 "axioms"
412 "class"
413 "classes"
414 "classrel"
415 "code_abort"
416 "code_class"
417 "code_const"
418 "code_datatype"
419 "code_include"
420 "code_instance"
421 "code_library"
422 "code_module"
423 "code_modulename"
424 "code_monad"
425 "code_reserved"
426 "code_type"
427 "coinductive"
428 "coinductive_set"
429 "constdefs"
430 "consts"
431 "consts_code"
432 "context"
433 "datatype"
434 "declaration"
435 "declare"
436 "defaultsort"
437 "defer_recdef"
438 "definition"
439 "defs"
440 "domain"
441 "equivariance"
442 "extract"
443 "extract_type"
444 "finalconsts"
445 "fixpat"
446 "fixrec"
447 "fun"
448 "global"
449 "hide"
450 "inductive"
451 "inductive_set"
452 "instantiation"
453 "judgment"
454 "lemmas"
455 "local"
456 "locale"
457 "method_setup"
458 "no_notation"
459 "no_syntax"
460 "no_translations"
461 "nominal_datatype"
462 "nonterminals"
463 "notation"
464 "oracle"
465 "overloading"
466 "parse_ast_translation"
467 "parse_translation"
468 "primrec"
469 "print_ast_translation"
470 "print_translation"
471 "quickcheck_params"
472 "realizability"
473 "realizers"
474 "recdef"
475 "record"
476 "refute_params"
477 "setup"
478 "simproc_setup"
479 "statespace"
480 "syntax"
481 "text"
482 "text_raw"
483 "theorems"
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)