| author | wenzelm |
| Tue, 06 Jun 2006 20:42:27 +0200 | |
| changeset 19797 | a527b3e1076a |
| parent 19655 | f10b141078e7 |
| child 19854 | 9c1732a66b0b |
| permissions | -rw-r--r-- |
1 ;;
2 ;; Keyword classification tables for Isabelle/Isar.
3 ;; This file was generated by Isabelle/ZF -- DO NOT EDIT!
4 ;;
5 ;; $Id$
6 ;;
8 (defconst isar-keywords-major
9 '("\\."
10 "\\.\\."
11 "ML"
12 "ML_command"
13 "ML_setup"
14 "ProofGeneral\\.context_thy_only"
15 "ProofGeneral\\.inform_file_processed"
16 "ProofGeneral\\.inform_file_retracted"
17 "ProofGeneral\\.kill_proof"
18 "ProofGeneral\\.process_pgip"
19 "ProofGeneral\\.redo"
20 "ProofGeneral\\.restart"
21 "ProofGeneral\\.try_context_thy_only"
22 "ProofGeneral\\.undo"
23 "abbreviation"
24 "also"
25 "apply"
26 "apply_end"
27 "arities"
28 "assume"
29 "axclass"
30 "axiomatization"
31 "axioms"
32 "back"
33 "by"
34 "cannot_undo"
35 "case"
36 "cd"
37 "chapter"
38 "class"
39 "classes"
40 "classrel"
41 "clear_undos"
42 "codatatype"
43 "code_alias"
44 "code_generate"
45 "code_library"
46 "code_module"
47 "code_primclass"
48 "code_primconst"
49 "code_primtyco"
50 "code_purge"
51 "code_serialize"
52 "code_syntax_const"
53 "code_syntax_tyco"
54 "coinductive"
55 "commit"
56 "const_syntax"
57 "constdefs"
58 "consts"
59 "consts_code"
60 "context"
61 "corollary"
62 "datatype"
63 "declare"
64 "def"
65 "defaultsort"
66 "defer"
67 "definition"
68 "defs"
69 "disable_pr"
70 "display_drafts"
71 "done"
72 "enable_pr"
73 "end"
74 "exit"
75 "extract"
76 "extract_type"
77 "finalconsts"
78 "finally"
79 "find_theorems"
80 "fix"
81 "from"
82 "full_prf"
83 "global"
84 "guess"
85 "have"
86 "header"
87 "hence"
88 "hide"
89 "inductive"
90 "inductive_cases"
91 "init_toplevel"
92 "instance"
93 "interpret"
94 "interpretation"
95 "invoke"
96 "judgment"
97 "kill"
98 "kill_thy"
99 "lemma"
100 "lemmas"
101 "let"
102 "local"
103 "locale"
104 "method_setup"
105 "moreover"
106 "next"
107 "no_syntax"
108 "no_translations"
109 "nonterminals"
110 "norm_by_eval"
111 "note"
112 "obtain"
113 "oops"
114 "oracle"
115 "parse_ast_translation"
116 "parse_translation"
117 "pr"
118 "prefer"
119 "presume"
120 "pretty_setmargin"
121 "prf"
122 "primrec"
123 "print_antiquotations"
124 "print_ast_translation"
125 "print_attributes"
126 "print_binds"
127 "print_cases"
128 "print_claset"
129 "print_commands"
130 "print_context"
131 "print_drafts"
132 "print_facts"
133 "print_induct_rules"
134 "print_interps"
135 "print_locale"
136 "print_locales"
137 "print_methods"
138 "print_rules"
139 "print_simpset"
140 "print_statement"
141 "print_syntax"
142 "print_tcset"
143 "print_theorems"
144 "print_theory"
145 "print_trans_rules"
146 "print_translation"
147 "proof"
148 "prop"
149 "pwd"
150 "qed"
151 "quickcheck"
152 "quickcheck_params"
153 "quit"
154 "realizability"
155 "realizers"
156 "redo"
157 "remove_thy"
158 "rep_datatype"
159 "sect"
160 "section"
161 "setup"
162 "show"
163 "sorry"
164 "subsect"
165 "subsection"
166 "subsubsect"
167 "subsubsection"
168 "syntax"
169 "term"
170 "text"
171 "text_raw"
172 "then"
173 "theorem"
174 "theorems"
175 "theory"
176 "thm"
177 "thm_deps"
178 "thus"
179 "token_translation"
180 "touch_all_thys"
181 "touch_child_thys"
182 "touch_thy"
183 "translations"
184 "txt"
185 "txt_raw"
186 "typ"
187 "typed_print_translation"
188 "typedecl"
189 "types"
190 "types_code"
191 "ultimately"
192 "undo"
193 "undos_proof"
194 "unfolding"
195 "update_thy"
196 "update_thy_only"
197 "use"
198 "use_thy"
199 "use_thy_only"
200 "using"
201 "value"
202 "welcome"
203 "with"
204 "{"
205 "}"))
207 (defconst isar-keywords-minor
208 '("advanced"
209 "and"
210 "assumes"
211 "attach"
212 "begin"
213 "binder"
214 "case_eqns"
215 "con_defs"
216 "concl"
217 "constrains"
218 "contains"
219 "defines"
220 "domains"
221 "elimination"
222 "file"
223 "fixes"
224 "for"
225 "if"
226 "imports"
227 "in"
228 "includes"
229 "induction"
230 "infix"
231 "infixl"
232 "infixr"
233 "intros"
234 "is"
235 "monos"
236 "notes"
237 "obtains"
238 "open"
239 "output"
240 "overloaded"
241 "recursor_eqns"
242 "shows"
243 "structure"
244 "target_atom"
245 "type_elims"
246 "type_intros"
247 "unchecked"
248 "uses"
249 "where"))
251 (defconst isar-keywords-control
252 '("ProofGeneral\\.context_thy_only"
253 "ProofGeneral\\.inform_file_processed"
254 "ProofGeneral\\.inform_file_retracted"
255 "ProofGeneral\\.kill_proof"
256 "ProofGeneral\\.process_pgip"
257 "ProofGeneral\\.redo"
258 "ProofGeneral\\.restart"
259 "ProofGeneral\\.try_context_thy_only"
260 "ProofGeneral\\.undo"
261 "cannot_undo"
262 "clear_undos"
263 "exit"
264 "init_toplevel"
265 "kill"
266 "quit"
267 "redo"
268 "undo"
269 "undos_proof"))
271 (defconst isar-keywords-diag
272 '("ML"
273 "ML_command"
274 "cd"
275 "commit"
276 "disable_pr"
277 "display_drafts"
278 "enable_pr"
279 "find_theorems"
280 "full_prf"
281 "header"
282 "kill_thy"
283 "pr"
284 "pretty_setmargin"
285 "prf"
286 "print_antiquotations"
287 "print_attributes"
288 "print_binds"
289 "print_cases"
290 "print_claset"
291 "print_commands"
292 "print_context"
293 "print_drafts"
294 "print_facts"
295 "print_induct_rules"
296 "print_interps"
297 "print_locale"
298 "print_locales"
299 "print_methods"
300 "print_rules"
301 "print_simpset"
302 "print_statement"
303 "print_syntax"
304 "print_tcset"
305 "print_theorems"
306 "print_theory"
307 "print_trans_rules"
308 "prop"
309 "pwd"
310 "quickcheck"
311 "remove_thy"
312 "term"
313 "thm"
314 "thm_deps"
315 "touch_all_thys"
316 "touch_child_thys"
317 "touch_thy"
318 "typ"
319 "update_thy"
320 "update_thy_only"
321 "use"
322 "use_thy"
323 "use_thy_only"
324 "value"
325 "welcome"))
327 (defconst isar-keywords-theory-begin
328 '("theory"))
330 (defconst isar-keywords-theory-switch
331 '("context"))
333 (defconst isar-keywords-theory-end
334 '("end"))
336 (defconst isar-keywords-theory-heading
337 '("chapter"
338 "section"
339 "subsection"
340 "subsubsection"))
342 (defconst isar-keywords-theory-decl
343 '("ML_setup"
344 "abbreviation"
345 "arities"
346 "axclass"
347 "axiomatization"
348 "axioms"
349 "class"
350 "classes"
351 "classrel"
352 "codatatype"
353 "code_alias"
354 "code_generate"
355 "code_library"
356 "code_module"
357 "code_primclass"
358 "code_primconst"
359 "code_primtyco"
360 "code_purge"
361 "code_serialize"
362 "code_syntax_const"
363 "code_syntax_tyco"
364 "coinductive"
365 "const_syntax"
366 "constdefs"
367 "consts"
368 "consts_code"
369 "datatype"
370 "defaultsort"
371 "definition"
372 "defs"
373 "extract"
374 "extract_type"
375 "finalconsts"
376 "global"
377 "hide"
378 "inductive"
379 "judgment"
380 "lemmas"
381 "local"
382 "locale"
383 "method_setup"
384 "no_syntax"
385 "no_translations"
386 "nonterminals"
387 "norm_by_eval"
388 "oracle"
389 "parse_ast_translation"
390 "parse_translation"
391 "primrec"
392 "print_ast_translation"
393 "print_translation"
394 "quickcheck_params"
395 "realizability"
396 "realizers"
397 "rep_datatype"
398 "setup"
399 "syntax"
400 "text"
401 "text_raw"
402 "theorems"
403 "token_translation"
404 "translations"
405 "typed_print_translation"
406 "typedecl"
407 "types"
408 "types_code"))
410 (defconst isar-keywords-theory-script
411 '("declare"
412 "inductive_cases"))
414 (defconst isar-keywords-theory-goal
415 '("corollary"
416 "instance"
417 "interpretation"
418 "lemma"
419 "theorem"))
421 (defconst isar-keywords-qed
422 '("\\."
423 "\\.\\."
424 "by"
425 "done"
426 "sorry"))
428 (defconst isar-keywords-qed-block
429 '("qed"))
431 (defconst isar-keywords-qed-global
432 '("oops"))
434 (defconst isar-keywords-proof-heading
435 '("sect"
436 "subsect"
437 "subsubsect"))
439 (defconst isar-keywords-proof-goal
440 '("have"
441 "hence"
442 "interpret"
443 "invoke"
444 "show"
445 "thus"))
447 (defconst isar-keywords-proof-block
448 '("next"
449 "proof"))
451 (defconst isar-keywords-proof-open
452 '("{"))
454 (defconst isar-keywords-proof-close
455 '("}"))
457 (defconst isar-keywords-proof-chain
458 '("finally"
459 "from"
460 "then"
461 "ultimately"
462 "with"))
464 (defconst isar-keywords-proof-decl
465 '("also"
466 "let"
467 "moreover"
468 "note"
469 "txt"
470 "txt_raw"
471 "unfolding"
472 "using"))
474 (defconst isar-keywords-proof-asm
475 '("assume"
476 "case"
477 "def"
478 "fix"
479 "presume"))
481 (defconst isar-keywords-proof-asm-goal
482 '("guess"
483 "obtain"))
485 (defconst isar-keywords-proof-script
486 '("apply"
487 "apply_end"
488 "back"
489 "defer"
490 "prefer"))
492 (provide 'isar-keywords)