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