| author | wenzelm |
| Fri, 14 Mar 2014 15:41:29 +0100 | |
| changeset 57488 | 8453d35e4684 |
| parent 57411 | 451d5b73f8cf |
| child 57617 | 600f432ab556 |
| permissions | -rw-r--r-- |
1 ;;
2 ;; Keyword classification tables for Isabelle/Isar.
3 ;; Generated from Pure + ZF.
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
5 ;;
7 (defconst isar-keywords-major
8 '("\\."
9 "\\.\\."
10 "Isabelle\\.command"
11 "ML"
12 "ML_command"
13 "ML_file"
14 "ML_prf"
15 "ML_val"
16 "ProofGeneral\\.inform_file_processed"
17 "ProofGeneral\\.inform_file_retracted"
18 "ProofGeneral\\.kill_proof"
19 "ProofGeneral\\.pr"
20 "ProofGeneral\\.process_pgip"
21 "ProofGeneral\\.restart"
22 "ProofGeneral\\.undo"
23 "abbreviation"
24 "also"
25 "apply"
26 "apply_end"
27 "assume"
28 "attribute_setup"
29 "axiomatization"
30 "back"
31 "bundle"
32 "by"
33 "cannot_undo"
34 "case"
35 "cd"
36 "chapter"
37 "class"
38 "class_deps"
39 "codatatype"
40 "code_datatype"
41 "coinductive"
42 "commit"
43 "consts"
44 "context"
45 "corollary"
46 "datatype"
47 "declaration"
48 "declare"
49 "def"
50 "default_sort"
51 "defer"
52 "definition"
53 "defs"
54 "disable_pr"
55 "display_drafts"
56 "done"
57 "enable_pr"
58 "end"
59 "exit"
60 "extract"
61 "extract_type"
62 "finally"
63 "find_consts"
64 "find_theorems"
65 "fix"
66 "from"
67 "full_prf"
68 "guess"
69 "have"
70 "header"
71 "help"
72 "hence"
73 "hide_class"
74 "hide_const"
75 "hide_fact"
76 "hide_type"
77 "include"
78 "including"
79 "inductive"
80 "inductive_cases"
81 "init_toplevel"
82 "instance"
83 "instantiation"
84 "interpret"
85 "interpretation"
86 "judgment"
87 "kill"
88 "kill_thy"
89 "lemma"
90 "lemmas"
91 "let"
92 "linear_undo"
93 "local_setup"
94 "locale"
95 "locale_deps"
96 "method_setup"
97 "moreover"
98 "next"
99 "no_notation"
100 "no_syntax"
101 "no_translations"
102 "no_type_notation"
103 "nonterminal"
104 "notation"
105 "note"
106 "notepad"
107 "obtain"
108 "oops"
109 "oracle"
110 "overloading"
111 "parse_ast_translation"
112 "parse_translation"
113 "pr"
114 "prefer"
115 "presume"
116 "pretty_setmargin"
117 "prf"
118 "primrec"
119 "print_ML_antiquotations"
120 "print_abbrevs"
121 "print_antiquotations"
122 "print_ast_translation"
123 "print_attributes"
124 "print_binds"
125 "print_bundles"
126 "print_cases"
127 "print_claset"
128 "print_classes"
129 "print_codesetup"
130 "print_commands"
131 "print_context"
132 "print_defn_rules"
133 "print_dependencies"
134 "print_facts"
135 "print_induct_rules"
136 "print_interps"
137 "print_locale"
138 "print_locales"
139 "print_methods"
140 "print_options"
141 "print_rules"
142 "print_simpset"
143 "print_state"
144 "print_statement"
145 "print_syntax"
146 "print_tcset"
147 "print_theorems"
148 "print_theory"
149 "print_trans_rules"
150 "print_translation"
151 "proof"
152 "prop"
153 "pwd"
154 "qed"
155 "quit"
156 "realizability"
157 "realizers"
158 "remove_thy"
159 "rep_datatype"
160 "schematic_corollary"
161 "schematic_lemma"
162 "schematic_theorem"
163 "sect"
164 "section"
165 "setup"
166 "show"
167 "simproc_setup"
168 "sorry"
169 "subclass"
170 "sublocale"
171 "subsect"
172 "subsection"
173 "subsubsect"
174 "subsubsection"
175 "syntax"
176 "syntax_declaration"
177 "term"
178 "text"
179 "text_raw"
180 "then"
181 "theorem"
182 "theorems"
183 "theory"
184 "thm"
185 "thm_deps"
186 "thus"
187 "thy_deps"
188 "translations"
189 "txt"
190 "txt_raw"
191 "typ"
192 "type_notation"
193 "type_synonym"
194 "typed_print_translation"
195 "typedecl"
196 "ultimately"
197 "undo"
198 "undos_proof"
199 "unfolding"
200 "unused_thms"
201 "use_thy"
202 "using"
203 "welcome"
204 "with"
205 "write"
206 "{"
207 "}"))
209 (defconst isar-keywords-minor
210 '("and"
211 "assumes"
212 "attach"
213 "begin"
214 "binder"
215 "case_eqns"
216 "con_defs"
217 "constrains"
218 "defines"
219 "domains"
220 "elimination"
221 "fixes"
222 "for"
223 "identifier"
224 "if"
225 "imports"
226 "in"
227 "includes"
228 "induction"
229 "infix"
230 "infixl"
231 "infixr"
232 "intros"
233 "is"
234 "keywords"
235 "monos"
236 "notes"
237 "obtains"
238 "open"
239 "output"
240 "overloaded"
241 "pervasive"
242 "recursor_eqns"
243 "shows"
244 "structure"
245 "type_elims"
246 "type_intros"
247 "unchecked"
248 "where"))
250 (defconst isar-keywords-control
251 '("Isabelle\\.command"
252 "ProofGeneral\\.inform_file_processed"
253 "ProofGeneral\\.inform_file_retracted"
254 "ProofGeneral\\.kill_proof"
255 "ProofGeneral\\.pr"
256 "ProofGeneral\\.process_pgip"
257 "ProofGeneral\\.restart"
258 "ProofGeneral\\.undo"
259 "cannot_undo"
260 "cd"
261 "commit"
262 "disable_pr"
263 "enable_pr"
264 "exit"
265 "init_toplevel"
266 "kill"
267 "kill_thy"
268 "linear_undo"
269 "pretty_setmargin"
270 "quit"
271 "remove_thy"
272 "undo"
273 "undos_proof"
274 "use_thy"))
276 (defconst isar-keywords-diag
277 '("ML_command"
278 "ML_val"
279 "class_deps"
280 "display_drafts"
281 "find_consts"
282 "find_theorems"
283 "full_prf"
284 "header"
285 "help"
286 "locale_deps"
287 "pr"
288 "prf"
289 "print_ML_antiquotations"
290 "print_abbrevs"
291 "print_antiquotations"
292 "print_attributes"
293 "print_binds"
294 "print_bundles"
295 "print_cases"
296 "print_claset"
297 "print_classes"
298 "print_codesetup"
299 "print_commands"
300 "print_context"
301 "print_defn_rules"
302 "print_dependencies"
303 "print_facts"
304 "print_induct_rules"
305 "print_interps"
306 "print_locale"
307 "print_locales"
308 "print_methods"
309 "print_options"
310 "print_rules"
311 "print_simpset"
312 "print_state"
313 "print_statement"
314 "print_syntax"
315 "print_tcset"
316 "print_theorems"
317 "print_theory"
318 "print_trans_rules"
319 "prop"
320 "pwd"
321 "term"
322 "thm"
323 "thm_deps"
324 "thy_deps"
325 "typ"
326 "unused_thms"
327 "welcome"))
329 (defconst isar-keywords-theory-begin
330 '("theory"))
332 (defconst isar-keywords-theory-switch
333 '())
335 (defconst isar-keywords-theory-end
336 '("end"))
338 (defconst isar-keywords-theory-heading
339 '("chapter"
340 "section"
341 "subsection"
342 "subsubsection"))
344 (defconst isar-keywords-theory-decl
345 '("ML"
346 "ML_file"
347 "abbreviation"
348 "attribute_setup"
349 "axiomatization"
350 "bundle"
351 "class"
352 "codatatype"
353 "code_datatype"
354 "coinductive"
355 "consts"
356 "context"
357 "datatype"
358 "declaration"
359 "declare"
360 "default_sort"
361 "definition"
362 "defs"
363 "extract"
364 "extract_type"
365 "hide_class"
366 "hide_const"
367 "hide_fact"
368 "hide_type"
369 "inductive"
370 "inductive_cases"
371 "instantiation"
372 "judgment"
373 "lemmas"
374 "local_setup"
375 "locale"
376 "method_setup"
377 "no_notation"
378 "no_syntax"
379 "no_translations"
380 "no_type_notation"
381 "nonterminal"
382 "notation"
383 "notepad"
384 "oracle"
385 "overloading"
386 "parse_ast_translation"
387 "parse_translation"
388 "primrec"
389 "print_ast_translation"
390 "print_translation"
391 "realizability"
392 "realizers"
393 "rep_datatype"
394 "setup"
395 "simproc_setup"
396 "syntax"
397 "syntax_declaration"
398 "text"
399 "text_raw"
400 "theorems"
401 "translations"
402 "type_notation"
403 "type_synonym"
404 "typed_print_translation"
405 "typedecl"))
407 (defconst isar-keywords-theory-script
408 '())
410 (defconst isar-keywords-theory-goal
411 '("corollary"
412 "instance"
413 "interpretation"
414 "lemma"
415 "schematic_corollary"
416 "schematic_lemma"
417 "schematic_theorem"
418 "subclass"
419 "sublocale"
420 "theorem"))
422 (defconst isar-keywords-qed
423 '("\\."
424 "\\.\\."
425 "by"
426 "done"
427 "sorry"))
429 (defconst isar-keywords-qed-block
430 '("qed"))
432 (defconst isar-keywords-qed-global
433 '("oops"))
435 (defconst isar-keywords-proof-heading
436 '("sect"
437 "subsect"
438 "subsubsect"))
440 (defconst isar-keywords-proof-goal
441 '("have"
442 "hence"
443 "interpret"))
445 (defconst isar-keywords-proof-block
446 '("next"
447 "proof"))
449 (defconst isar-keywords-proof-open
450 '("{"))
452 (defconst isar-keywords-proof-close
453 '("}"))
455 (defconst isar-keywords-proof-chain
456 '("finally"
457 "from"
458 "then"
459 "ultimately"
460 "with"))
462 (defconst isar-keywords-proof-decl
463 '("ML_prf"
464 "also"
465 "include"
466 "including"
467 "let"
468 "moreover"
469 "note"
470 "txt"
471 "txt_raw"
472 "unfolding"
473 "using"
474 "write"))
476 (defconst isar-keywords-proof-asm
477 '("assume"
478 "case"
479 "def"
480 "fix"
481 "presume"))
483 (defconst isar-keywords-proof-asm-goal
484 '("guess"
485 "obtain"
486 "show"
487 "thus"))
489 (defconst isar-keywords-proof-script
490 '("apply"
491 "apply_end"
492 "back"
493 "defer"
494 "prefer"))
496 (provide 'isar-keywords)