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