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