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