| author | nipkow |
| Mon, 13 Dec 2004 17:07:47 +0100 | |
| changeset 15405 | 010ea63b7a67 |
| parent 15141 | a95c2ff210ba |
| child 15596 | 8665d08085df |
| 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\\.context_thy_only"
15 "ProofGeneral\\.inform_file_processed"
16 "ProofGeneral\\.inform_file_retracted"
17 "ProofGeneral\\.kill_proof"
18 "ProofGeneral\\.process_pgip"
19 "ProofGeneral\\.restart"
20 "ProofGeneral\\.try_context_thy_only"
21 "ProofGeneral\\.undo"
22 "also"
23 "apply"
24 "apply_end"
25 "arities"
26 "assume"
27 "automaton"
28 "ax_specification"
29 "axclass"
30 "axioms"
31 "back"
32 "by"
33 "cannot_undo"
34 "case"
35 "cd"
36 "chapter"
37 "classes"
38 "classrel"
39 "clear_undos"
40 "coinductive"
41 "commit"
42 "constdefs"
43 "consts"
44 "consts_code"
45 "context"
46 "corollary"
47 "datatype"
48 "declare"
49 "def"
50 "defaultsort"
51 "defer"
52 "defer_recdef"
53 "defs"
54 "disable_pr"
55 "display_drafts"
56 "domain"
57 "done"
58 "enable_pr"
59 "end"
60 "exit"
61 "extract"
62 "extract_type"
63 "finalconsts"
64 "finally"
65 "find_rewrites"
66 "fix"
67 "from"
68 "full_prf"
69 "generate_code"
70 "global"
71 "have"
72 "header"
73 "hence"
74 "hide"
75 "inductive"
76 "inductive_cases"
77 "init_toplevel"
78 "instance"
79 "instantiate"
80 "judgment"
81 "kill"
82 "kill_thy"
83 "lemma"
84 "lemmas"
85 "let"
86 "local"
87 "locale"
88 "method_setup"
89 "moreover"
90 "next"
91 "nonterminals"
92 "note"
93 "obtain"
94 "oops"
95 "oracle"
96 "parse_ast_translation"
97 "parse_translation"
98 "pr"
99 "prefer"
100 "presume"
101 "pretty_setmargin"
102 "prf"
103 "primrec"
104 "print_antiquotations"
105 "print_ast_translation"
106 "print_attributes"
107 "print_binds"
108 "print_cases"
109 "print_claset"
110 "print_commands"
111 "print_context"
112 "print_drafts"
113 "print_facts"
114 "print_induct_rules"
115 "print_intros"
116 "print_locale"
117 "print_locales"
118 "print_methods"
119 "print_rules"
120 "print_simpset"
121 "print_syntax"
122 "print_theorems"
123 "print_theory"
124 "print_trans_rules"
125 "print_translation"
126 "proof"
127 "prop"
128 "pwd"
129 "qed"
130 "quickcheck"
131 "quickcheck_params"
132 "quit"
133 "realizability"
134 "realizers"
135 "recdef"
136 "recdef_tc"
137 "record"
138 "redo"
139 "refute"
140 "refute_params"
141 "remove_thy"
142 "rep_datatype"
143 "sect"
144 "section"
145 "setup"
146 "show"
147 "sorry"
148 "specification"
149 "subsect"
150 "subsection"
151 "subsubsect"
152 "subsubsection"
153 "syntax"
154 "term"
155 "text"
156 "text_raw"
157 "then"
158 "theorem"
159 "theorems"
160 "theory"
161 "thm"
162 "thm_deps"
163 "thms_containing"
164 "thus"
165 "token_translation"
166 "touch_all_thys"
167 "touch_child_thys"
168 "touch_thy"
169 "translations"
170 "txt"
171 "txt_raw"
172 "typ"
173 "typed_print_translation"
174 "typedecl"
175 "typedef"
176 "types"
177 "types_code"
178 "ultimately"
179 "undo"
180 "undos_proof"
181 "update_thy"
182 "update_thy_only"
183 "use"
184 "use_thy"
185 "use_thy_only"
186 "using"
187 "welcome"
188 "with"
189 "{"
190 "}"))
192 (defconst isar-keywords-minor
193 '("actions"
194 "advanced"
195 "and"
196 "assumes"
197 "begin"
198 "binder"
199 "compose"
200 "concl"
201 "congs"
202 "defines"
203 "distinct"
204 "files"
205 "fixes"
206 "hide_action"
207 "hints"
208 "imports"
209 "in"
210 "includes"
211 "induction"
212 "infix"
213 "infixl"
214 "infixr"
215 "initially"
216 "inject"
217 "inputs"
218 "internals"
219 "intros"
220 "is"
221 "lazy"
222 "monos"
223 "morphisms"
224 "notes"
225 "open"
226 "output"
227 "outputs"
228 "overloaded"
229 "permissive"
230 "post"
231 "pre"
232 "rename"
233 "restrict"
234 "shows"
235 "signature"
236 "states"
237 "structure"
238 "to"
239 "transitions"
240 "transrel"
241 "where"))
243 (defconst isar-keywords-control
244 '("ProofGeneral\\.context_thy_only"
245 "ProofGeneral\\.inform_file_processed"
246 "ProofGeneral\\.inform_file_retracted"
247 "ProofGeneral\\.kill_proof"
248 "ProofGeneral\\.process_pgip"
249 "ProofGeneral\\.restart"
250 "ProofGeneral\\.try_context_thy_only"
251 "ProofGeneral\\.undo"
252 "cannot_undo"
253 "clear_undos"
254 "exit"
255 "init_toplevel"
256 "kill"
257 "quit"
258 "redo"
259 "undo"
260 "undos_proof"))
262 (defconst isar-keywords-diag
263 '("ML"
264 "ML_command"
265 "cd"
266 "commit"
267 "disable_pr"
268 "display_drafts"
269 "enable_pr"
270 "find_rewrites"
271 "full_prf"
272 "header"
273 "kill_thy"
274 "pr"
275 "pretty_setmargin"
276 "prf"
277 "print_antiquotations"
278 "print_attributes"
279 "print_binds"
280 "print_cases"
281 "print_claset"
282 "print_commands"
283 "print_context"
284 "print_drafts"
285 "print_facts"
286 "print_induct_rules"
287 "print_intros"
288 "print_locale"
289 "print_locales"
290 "print_methods"
291 "print_rules"
292 "print_simpset"
293 "print_syntax"
294 "print_theorems"
295 "print_theory"
296 "print_trans_rules"
297 "prop"
298 "pwd"
299 "quickcheck"
300 "refute"
301 "remove_thy"
302 "term"
303 "thm"
304 "thm_deps"
305 "thms_containing"
306 "touch_all_thys"
307 "touch_child_thys"
308 "touch_thy"
309 "typ"
310 "update_thy"
311 "update_thy_only"
312 "use"
313 "use_thy"
314 "use_thy_only"
315 "welcome"))
317 (defconst isar-keywords-theory-begin
318 '("theory"))
320 (defconst isar-keywords-theory-switch
321 '("context"))
323 (defconst isar-keywords-theory-end
324 '("end"))
326 (defconst isar-keywords-theory-heading
327 '("chapter"
328 "section"
329 "subsection"
330 "subsubsection"))
332 (defconst isar-keywords-theory-decl
333 '("ML_setup"
334 "arities"
335 "automaton"
336 "axclass"
337 "axioms"
338 "classes"
339 "classrel"
340 "coinductive"
341 "constdefs"
342 "consts"
343 "consts_code"
344 "datatype"
345 "defaultsort"
346 "defer_recdef"
347 "defs"
348 "domain"
349 "extract"
350 "extract_type"
351 "finalconsts"
352 "generate_code"
353 "global"
354 "hide"
355 "inductive"
356 "judgment"
357 "lemmas"
358 "local"
359 "locale"
360 "method_setup"
361 "nonterminals"
362 "oracle"
363 "parse_ast_translation"
364 "parse_translation"
365 "primrec"
366 "print_ast_translation"
367 "print_translation"
368 "quickcheck_params"
369 "realizability"
370 "realizers"
371 "recdef"
372 "record"
373 "refute_params"
374 "rep_datatype"
375 "setup"
376 "syntax"
377 "text"
378 "text_raw"
379 "theorems"
380 "token_translation"
381 "translations"
382 "typed_print_translation"
383 "typedecl"
384 "types"
385 "types_code"))
387 (defconst isar-keywords-theory-script
388 '("declare"
389 "inductive_cases"))
391 (defconst isar-keywords-theory-goal
392 '("ax_specification"
393 "corollary"
394 "instance"
395 "lemma"
396 "recdef_tc"
397 "specification"
398 "theorem"
399 "typedef"))
401 (defconst isar-keywords-qed
402 '("\\."
403 "\\.\\."
404 "by"
405 "done"
406 "sorry"))
408 (defconst isar-keywords-qed-block
409 '("qed"))
411 (defconst isar-keywords-qed-global
412 '("oops"))
414 (defconst isar-keywords-proof-heading
415 '("sect"
416 "subsect"
417 "subsubsect"))
419 (defconst isar-keywords-proof-goal
420 '("have"
421 "hence"
422 "show"
423 "thus"))
425 (defconst isar-keywords-proof-block
426 '("next"
427 "proof"))
429 (defconst isar-keywords-proof-open
430 '("{"))
432 (defconst isar-keywords-proof-close
433 '("}"))
435 (defconst isar-keywords-proof-chain
436 '("finally"
437 "from"
438 "then"
439 "ultimately"
440 "with"))
442 (defconst isar-keywords-proof-decl
443 '("also"
444 "instantiate"
445 "let"
446 "moreover"
447 "note"
448 "txt"
449 "txt_raw"
450 "using"))
452 (defconst isar-keywords-proof-asm
453 '("assume"
454 "case"
455 "def"
456 "fix"
457 "presume"))
459 (defconst isar-keywords-proof-asm-goal
460 '("obtain"))
462 (defconst isar-keywords-proof-script
463 '("apply"
464 "apply_end"
465 "back"
466 "defer"
467 "prefer"))
469 (provide 'isar-keywords)