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