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