| author | haftmann |
| Mon, 20 Aug 2007 18:07:26 +0200 | |
| changeset 24343 | acc0f7aac619 |
| parent 24249 | 1f60b45c5f97 |
| child 24437 | c2a76e8a3d54 |
| 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\\.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 "atom_decl"
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_instance"
48 "code_library"
49 "code_module"
50 "code_modulename"
51 "code_moduleprolog"
52 "code_monad"
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 "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 "done"
76 "enable_pr"
77 "end"
78 "equivariance"
79 "exit"
80 "export_code"
81 "extract"
82 "extract_type"
83 "finalconsts"
84 "finally"
85 "find_theorems"
86 "fix"
87 "from"
88 "full_prf"
89 "fun"
90 "function"
91 "global"
92 "guess"
93 "have"
94 "header"
95 "help"
96 "hence"
97 "hide"
98 "inductive"
99 "inductive_cases"
100 "inductive_set"
101 "init_toplevel"
102 "instance"
103 "interpret"
104 "interpretation"
105 "invoke"
106 "judgment"
107 "kill"
108 "kill_thy"
109 "lemma"
110 "lemmas"
111 "let"
112 "local"
113 "locale"
114 "method_setup"
115 "moreover"
116 "next"
117 "no_syntax"
118 "no_translations"
119 "nominal_datatype"
120 "nominal_inductive"
121 "nominal_primrec"
122 "nonterminals"
123 "normal_form"
124 "notation"
125 "note"
126 "obtain"
127 "oops"
128 "oracle"
129 "parse_ast_translation"
130 "parse_translation"
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_atp_rules"
141 "print_attributes"
142 "print_binds"
143 "print_cases"
144 "print_claset"
145 "print_classes"
146 "print_codesetup"
147 "print_commands"
148 "print_configs"
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_noatp_rules"
158 "print_rules"
159 "print_simpset"
160 "print_statement"
161 "print_syntax"
162 "print_theorems"
163 "print_theory"
164 "print_trans_rules"
165 "print_translation"
166 "proof"
167 "prop"
168 "pwd"
169 "qed"
170 "quickcheck"
171 "quickcheck_params"
172 "quit"
173 "realizability"
174 "realizers"
175 "recdef"
176 "recdef_tc"
177 "record"
178 "redo"
179 "refute"
180 "refute_params"
181 "remove_thy"
182 "rep_datatype"
183 "sect"
184 "section"
185 "setup"
186 "show"
187 "simproc_setup"
188 "sledgehammer"
189 "sorry"
190 "specification"
191 "subsect"
192 "subsection"
193 "subsubsect"
194 "subsubsection"
195 "syntax"
196 "term"
197 "termination"
198 "text"
199 "text_raw"
200 "then"
201 "theorem"
202 "theorems"
203 "theory"
204 "thm"
205 "thm_deps"
206 "thus"
207 "thy_deps"
208 "token_translation"
209 "touch_child_thys"
210 "touch_thy"
211 "translations"
212 "txt"
213 "txt_raw"
214 "typ"
215 "typed_print_translation"
216 "typedecl"
217 "typedef"
218 "types"
219 "types_code"
220 "ultimately"
221 "undo"
222 "undos_proof"
223 "unfolding"
224 "use"
225 "use_thy"
226 "using"
227 "value"
228 "welcome"
229 "with"
230 "{"
231 "}"))
233 (defconst isar-keywords-minor
234 '("advanced"
235 "and"
236 "assumes"
237 "attach"
238 "avoids"
239 "begin"
240 "binder"
241 "concl"
242 "congs"
243 "constrains"
244 "contains"
245 "defines"
246 "distinct"
247 "file"
248 "fixes"
249 "for"
250 "freshness_context"
251 "hints"
252 "identifier"
253 "if"
254 "imports"
255 "in"
256 "includes"
257 "induction"
258 "infix"
259 "infixl"
260 "infixr"
261 "inject"
262 "invariant"
263 "is"
264 "module_name"
265 "monos"
266 "morphisms"
267 "notes"
268 "obtains"
269 "open"
270 "otherwise"
271 "output"
272 "overloaded"
273 "permissive"
274 "sequential"
275 "shows"
276 "structure"
277 "unchecked"
278 "uses"
279 "where"))
281 (defconst isar-keywords-control
282 '("ProofGeneral\\.inform_file_processed"
283 "ProofGeneral\\.inform_file_retracted"
284 "ProofGeneral\\.kill_proof"
285 "ProofGeneral\\.process_pgip"
286 "ProofGeneral\\.restart"
287 "ProofGeneral\\.undo"
288 "cannot_undo"
289 "exit"
290 "init_toplevel"
291 "kill"
292 "quit"
293 "redo"
294 "undo"
295 "undos_proof"))
297 (defconst isar-keywords-diag
298 '("ML"
299 "ML_command"
300 "cd"
301 "class_deps"
302 "code_deps"
303 "code_thms"
304 "commit"
305 "disable_pr"
306 "display_drafts"
307 "enable_pr"
308 "export_code"
309 "find_theorems"
310 "full_prf"
311 "header"
312 "help"
313 "kill_thy"
314 "normal_form"
315 "pr"
316 "pretty_setmargin"
317 "prf"
318 "print_abbrevs"
319 "print_antiquotations"
320 "print_atp_rules"
321 "print_attributes"
322 "print_binds"
323 "print_cases"
324 "print_claset"
325 "print_classes"
326 "print_codesetup"
327 "print_commands"
328 "print_configs"
329 "print_context"
330 "print_drafts"
331 "print_facts"
332 "print_induct_rules"
333 "print_interps"
334 "print_locale"
335 "print_locales"
336 "print_methods"
337 "print_noatp_rules"
338 "print_rules"
339 "print_simpset"
340 "print_statement"
341 "print_syntax"
342 "print_theorems"
343 "print_theory"
344 "print_trans_rules"
345 "prop"
346 "pwd"
347 "quickcheck"
348 "refute"
349 "remove_thy"
350 "sledgehammer"
351 "term"
352 "thm"
353 "thm_deps"
354 "thy_deps"
355 "touch_child_thys"
356 "touch_thy"
357 "typ"
358 "use"
359 "use_thy"
360 "value"
361 "welcome"))
363 (defconst isar-keywords-theory-begin
364 '("theory"))
366 (defconst isar-keywords-theory-switch
367 '())
369 (defconst isar-keywords-theory-end
370 '("end"))
372 (defconst isar-keywords-theory-heading
373 '("chapter"
374 "section"
375 "subsection"
376 "subsubsection"))
378 (defconst isar-keywords-theory-decl
379 '("ML_setup"
380 "abbreviation"
381 "arities"
382 "atom_decl"
383 "axclass"
384 "axiomatization"
385 "axioms"
386 "class"
387 "classes"
388 "classrel"
389 "code_abstype"
390 "code_axioms"
391 "code_class"
392 "code_const"
393 "code_datatype"
394 "code_instance"
395 "code_library"
396 "code_module"
397 "code_modulename"
398 "code_moduleprolog"
399 "code_monad"
400 "code_reserved"
401 "code_type"
402 "coinductive"
403 "coinductive_set"
404 "constdefs"
405 "consts"
406 "consts_code"
407 "context"
408 "datatype"
409 "declaration"
410 "declare"
411 "defaultsort"
412 "defer_recdef"
413 "definition"
414 "defs"
415 "equivariance"
416 "extract"
417 "extract_type"
418 "finalconsts"
419 "fun"
420 "global"
421 "hide"
422 "inductive"
423 "inductive_set"
424 "judgment"
425 "lemmas"
426 "local"
427 "locale"
428 "method_setup"
429 "no_syntax"
430 "no_translations"
431 "nominal_datatype"
432 "nonterminals"
433 "notation"
434 "oracle"
435 "parse_ast_translation"
436 "parse_translation"
437 "primrec"
438 "print_ast_translation"
439 "print_translation"
440 "quickcheck_params"
441 "realizability"
442 "realizers"
443 "recdef"
444 "record"
445 "refute_params"
446 "rep_datatype"
447 "setup"
448 "simproc_setup"
449 "syntax"
450 "text"
451 "text_raw"
452 "theorems"
453 "token_translation"
454 "translations"
455 "typed_print_translation"
456 "typedecl"
457 "types"
458 "types_code"))
460 (defconst isar-keywords-theory-script
461 '("inductive_cases"))
463 (defconst isar-keywords-theory-goal
464 '("ax_specification"
465 "corollary"
466 "function"
467 "instance"
468 "interpretation"
469 "lemma"
470 "nominal_inductive"
471 "nominal_primrec"
472 "recdef_tc"
473 "specification"
474 "termination"
475 "theorem"
476 "typedef"))
478 (defconst isar-keywords-qed
479 '("\\."
480 "\\.\\."
481 "by"
482 "done"
483 "sorry"))
485 (defconst isar-keywords-qed-block
486 '("qed"))
488 (defconst isar-keywords-qed-global
489 '("oops"))
491 (defconst isar-keywords-proof-heading
492 '("sect"
493 "subsect"
494 "subsubsect"))
496 (defconst isar-keywords-proof-goal
497 '("have"
498 "hence"
499 "interpret"
500 "invoke"))
502 (defconst isar-keywords-proof-block
503 '("next"
504 "proof"))
506 (defconst isar-keywords-proof-open
507 '("{"))
509 (defconst isar-keywords-proof-close
510 '("}"))
512 (defconst isar-keywords-proof-chain
513 '("finally"
514 "from"
515 "then"
516 "ultimately"
517 "with"))
519 (defconst isar-keywords-proof-decl
520 '("also"
521 "let"
522 "moreover"
523 "note"
524 "txt"
525 "txt_raw"
526 "unfolding"
527 "using"))
529 (defconst isar-keywords-proof-asm
530 '("assume"
531 "case"
532 "def"
533 "fix"
534 "presume"))
536 (defconst isar-keywords-proof-asm-goal
537 '("guess"
538 "obtain"
539 "show"
540 "thus"))
542 (defconst isar-keywords-proof-script
543 '("apply"
544 "apply_end"
545 "back"
546 "defer"
547 "prefer"))
549 (provide 'isar-keywords)