| author | haftmann |
| Tue, 29 Aug 2006 14:31:11 +0200 | |
| changeset 20424 | d5b4b55ad277 |
| parent 20378 | 63a0aafc89ba |
| child 20453 | 855f07fabd76 |
| permissions | -rw-r--r-- |
1 ;;
2 ;; Keyword classification tables for Isabelle/Isar.
3 ;; This file was generated by Isabelle/HOL/HOL-Nominal -- 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 "atom_decl"
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 "classes"
43 "classrel"
44 "clear_undos"
45 "code_class"
46 "code_constapp"
47 "code_constname"
48 "code_generate"
49 "code_instance"
50 "code_library"
51 "code_module"
52 "code_purge"
53 "code_serialize"
54 "code_simtype"
55 "code_typapp"
56 "code_typename"
57 "coinductive"
58 "commit"
59 "const_syntax"
60 "constdefs"
61 "consts"
62 "consts_code"
63 "context"
64 "corollary"
65 "datatype"
66 "declare"
67 "def"
68 "defaultsort"
69 "defer"
70 "defer_recdef"
71 "definition"
72 "defs"
73 "disable_pr"
74 "display_drafts"
75 "done"
76 "enable_pr"
77 "end"
78 "exit"
79 "extract"
80 "extract_type"
81 "finalconsts"
82 "finally"
83 "find_theorems"
84 "fix"
85 "from"
86 "full_prf"
87 "function"
88 "global"
89 "guess"
90 "have"
91 "header"
92 "hence"
93 "hide"
94 "inductive"
95 "inductive_cases"
96 "init_toplevel"
97 "instance"
98 "interpret"
99 "interpretation"
100 "invoke"
101 "judgment"
102 "kill"
103 "kill_thy"
104 "lemma"
105 "lemmas"
106 "let"
107 "local"
108 "locale"
109 "method_setup"
110 "moreover"
111 "next"
112 "no_syntax"
113 "no_translations"
114 "nominal_datatype"
115 "nonterminals"
116 "normal_form"
117 "note"
118 "obtain"
119 "oops"
120 "oracle"
121 "parse_ast_translation"
122 "parse_translation"
123 "pr"
124 "prefer"
125 "presume"
126 "pretty_setmargin"
127 "prf"
128 "primrec"
129 "print_antiquotations"
130 "print_ast_translation"
131 "print_attributes"
132 "print_binds"
133 "print_cases"
134 "print_claset"
135 "print_classes"
136 "print_commands"
137 "print_context"
138 "print_drafts"
139 "print_facts"
140 "print_induct_rules"
141 "print_interps"
142 "print_locale"
143 "print_locales"
144 "print_methods"
145 "print_rules"
146 "print_simpset"
147 "print_statement"
148 "print_syntax"
149 "print_theorems"
150 "print_theory"
151 "print_trans_rules"
152 "print_translation"
153 "proof"
154 "prop"
155 "pwd"
156 "qed"
157 "quickcheck"
158 "quickcheck_params"
159 "quit"
160 "realizability"
161 "realizers"
162 "recdef"
163 "recdef_tc"
164 "record"
165 "redo"
166 "refute"
167 "refute_params"
168 "remove_thy"
169 "rep_datatype"
170 "sect"
171 "section"
172 "setup"
173 "show"
174 "sorry"
175 "specification"
176 "subsect"
177 "subsection"
178 "subsubsect"
179 "subsubsection"
180 "syntax"
181 "term"
182 "termination"
183 "text"
184 "text_raw"
185 "then"
186 "theorem"
187 "theorems"
188 "theory"
189 "thm"
190 "thm_deps"
191 "thus"
192 "token_translation"
193 "touch_all_thys"
194 "touch_child_thys"
195 "touch_thy"
196 "translations"
197 "txt"
198 "txt_raw"
199 "typ"
200 "typed_print_translation"
201 "typedecl"
202 "typedef"
203 "types"
204 "types_code"
205 "ultimately"
206 "undo"
207 "undos_proof"
208 "unfolding"
209 "update_thy"
210 "update_thy_only"
211 "use"
212 "use_thy"
213 "use_thy_only"
214 "using"
215 "value"
216 "welcome"
217 "with"
218 "{"
219 "}"))
221 (defconst isar-keywords-minor
222 '("advanced"
223 "and"
224 "assumes"
225 "attach"
226 "begin"
227 "binder"
228 "concl"
229 "congs"
230 "constrains"
231 "contains"
232 "defines"
233 "distinct"
234 "file"
235 "fixes"
236 "for"
237 "hints"
238 "if"
239 "imports"
240 "in"
241 "includes"
242 "induction"
243 "infix"
244 "infixl"
245 "infixr"
246 "inject"
247 "intros"
248 "is"
249 "monos"
250 "morphisms"
251 "notes"
252 "obtains"
253 "open"
254 "otherwise"
255 "output"
256 "overloaded"
257 "permissive"
258 "sequential"
259 "shows"
260 "structure"
261 "target_atom"
262 "unchecked"
263 "uses"
264 "where"))
266 (defconst isar-keywords-control
267 '("ProofGeneral\\.context_thy_only"
268 "ProofGeneral\\.inform_file_processed"
269 "ProofGeneral\\.inform_file_retracted"
270 "ProofGeneral\\.kill_proof"
271 "ProofGeneral\\.process_pgip"
272 "ProofGeneral\\.redo"
273 "ProofGeneral\\.restart"
274 "ProofGeneral\\.try_context_thy_only"
275 "ProofGeneral\\.undo"
276 "cannot_undo"
277 "clear_undos"
278 "exit"
279 "init_toplevel"
280 "kill"
281 "quit"
282 "redo"
283 "undo"
284 "undos_proof"))
286 (defconst isar-keywords-diag
287 '("ML"
288 "ML_command"
289 "ProofGeneral\\.call_atp"
290 "cd"
291 "commit"
292 "disable_pr"
293 "display_drafts"
294 "enable_pr"
295 "find_theorems"
296 "full_prf"
297 "header"
298 "kill_thy"
299 "pr"
300 "pretty_setmargin"
301 "prf"
302 "print_antiquotations"
303 "print_attributes"
304 "print_binds"
305 "print_cases"
306 "print_claset"
307 "print_classes"
308 "print_commands"
309 "print_context"
310 "print_drafts"
311 "print_facts"
312 "print_induct_rules"
313 "print_interps"
314 "print_locale"
315 "print_locales"
316 "print_methods"
317 "print_rules"
318 "print_simpset"
319 "print_statement"
320 "print_syntax"
321 "print_theorems"
322 "print_theory"
323 "print_trans_rules"
324 "prop"
325 "pwd"
326 "quickcheck"
327 "refute"
328 "remove_thy"
329 "term"
330 "thm"
331 "thm_deps"
332 "touch_all_thys"
333 "touch_child_thys"
334 "touch_thy"
335 "typ"
336 "update_thy"
337 "update_thy_only"
338 "use"
339 "use_thy"
340 "use_thy_only"
341 "value"
342 "welcome"))
344 (defconst isar-keywords-theory-begin
345 '("theory"))
347 (defconst isar-keywords-theory-switch
348 '("context"))
350 (defconst isar-keywords-theory-end
351 '("end"))
353 (defconst isar-keywords-theory-heading
354 '("chapter"
355 "section"
356 "subsection"
357 "subsubsection"))
359 (defconst isar-keywords-theory-decl
360 '("ML_setup"
361 "abbreviation"
362 "arities"
363 "atom_decl"
364 "axclass"
365 "axiomatization"
366 "axioms"
367 "class"
368 "classes"
369 "classrel"
370 "code_class"
371 "code_constapp"
372 "code_constname"
373 "code_generate"
374 "code_instance"
375 "code_library"
376 "code_module"
377 "code_purge"
378 "code_serialize"
379 "code_typapp"
380 "code_typename"
381 "coinductive"
382 "const_syntax"
383 "constdefs"
384 "consts"
385 "consts_code"
386 "datatype"
387 "defaultsort"
388 "defer_recdef"
389 "definition"
390 "defs"
391 "extract"
392 "extract_type"
393 "finalconsts"
394 "global"
395 "hide"
396 "inductive"
397 "judgment"
398 "lemmas"
399 "local"
400 "locale"
401 "method_setup"
402 "no_syntax"
403 "no_translations"
404 "nominal_datatype"
405 "nonterminals"
406 "normal_form"
407 "oracle"
408 "parse_ast_translation"
409 "parse_translation"
410 "primrec"
411 "print_ast_translation"
412 "print_translation"
413 "quickcheck_params"
414 "realizability"
415 "realizers"
416 "recdef"
417 "record"
418 "refute_params"
419 "rep_datatype"
420 "setup"
421 "syntax"
422 "text"
423 "text_raw"
424 "theorems"
425 "token_translation"
426 "translations"
427 "typed_print_translation"
428 "typedecl"
429 "types"
430 "types_code"))
432 (defconst isar-keywords-theory-script
433 '("declare"
434 "inductive_cases"))
436 (defconst isar-keywords-theory-goal
437 '("ax_specification"
438 "code_simtype"
439 "corollary"
440 "function"
441 "instance"
442 "interpretation"
443 "lemma"
444 "recdef_tc"
445 "specification"
446 "termination"
447 "theorem"
448 "typedef"))
450 (defconst isar-keywords-qed
451 '("\\."
452 "\\.\\."
453 "by"
454 "done"
455 "sorry"))
457 (defconst isar-keywords-qed-block
458 '("qed"))
460 (defconst isar-keywords-qed-global
461 '("oops"))
463 (defconst isar-keywords-proof-heading
464 '("sect"
465 "subsect"
466 "subsubsect"))
468 (defconst isar-keywords-proof-goal
469 '("have"
470 "hence"
471 "interpret"
472 "invoke"
473 "show"
474 "thus"))
476 (defconst isar-keywords-proof-block
477 '("next"
478 "proof"))
480 (defconst isar-keywords-proof-open
481 '("{"))
483 (defconst isar-keywords-proof-close
484 '("}"))
486 (defconst isar-keywords-proof-chain
487 '("finally"
488 "from"
489 "then"
490 "ultimately"
491 "with"))
493 (defconst isar-keywords-proof-decl
494 '("also"
495 "let"
496 "moreover"
497 "note"
498 "txt"
499 "txt_raw"
500 "unfolding"
501 "using"))
503 (defconst isar-keywords-proof-asm
504 '("assume"
505 "case"
506 "def"
507 "fix"
508 "presume"))
510 (defconst isar-keywords-proof-asm-goal
511 '("guess"
512 "obtain"))
514 (defconst isar-keywords-proof-script
515 '("apply"
516 "apply_end"
517 "back"
518 "defer"
519 "prefer"))
521 (provide 'isar-keywords)