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