| author | wenzelm |
| Mon, 10 Feb 2014 22:08:18 +0100 | |
| changeset 56727 | 169e12bbf9a3 |
| parent 53686 | 802576856527 |
| child 57411 | 451d5b73f8cf |
| 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_abbrevs"
120 "print_antiquotations"
121 "print_ast_translation"
122 "print_attributes"
123 "print_binds"
124 "print_bundles"
125 "print_cases"
126 "print_claset"
127 "print_classes"
128 "print_codesetup"
129 "print_commands"
130 "print_context"
131 "print_defn_rules"
132 "print_dependencies"
133 "print_facts"
134 "print_induct_rules"
135 "print_interps"
136 "print_locale"
137 "print_locales"
138 "print_methods"
139 "print_options"
140 "print_rules"
141 "print_simpset"
142 "print_state"
143 "print_statement"
144 "print_syntax"
145 "print_tcset"
146 "print_theorems"
147 "print_theory"
148 "print_trans_rules"
149 "print_translation"
150 "proof"
151 "prop"
152 "pwd"
153 "qed"
154 "quit"
155 "realizability"
156 "realizers"
157 "remove_thy"
158 "rep_datatype"
159 "schematic_corollary"
160 "schematic_lemma"
161 "schematic_theorem"
162 "sect"
163 "section"
164 "setup"
165 "show"
166 "simproc_setup"
167 "sorry"
168 "subclass"
169 "sublocale"
170 "subsect"
171 "subsection"
172 "subsubsect"
173 "subsubsection"
174 "syntax"
175 "syntax_declaration"
176 "term"
177 "text"
178 "text_raw"
179 "then"
180 "theorem"
181 "theorems"
182 "theory"
183 "thm"
184 "thm_deps"
185 "thus"
186 "thy_deps"
187 "translations"
188 "txt"
189 "txt_raw"
190 "typ"
191 "type_notation"
192 "type_synonym"
193 "typed_print_translation"
194 "typedecl"
195 "ultimately"
196 "undo"
197 "undos_proof"
198 "unfolding"
199 "unused_thms"
200 "use_thy"
201 "using"
202 "welcome"
203 "with"
204 "write"
205 "{"
206 "}"))
208 (defconst isar-keywords-minor
209 '("and"
210 "assumes"
211 "attach"
212 "begin"
213 "binder"
214 "case_eqns"
215 "con_defs"
216 "constrains"
217 "defines"
218 "domains"
219 "elimination"
220 "fixes"
221 "for"
222 "identifier"
223 "if"
224 "imports"
225 "in"
226 "includes"
227 "induction"
228 "infix"
229 "infixl"
230 "infixr"
231 "intros"
232 "is"
233 "keywords"
234 "monos"
235 "notes"
236 "obtains"
237 "open"
238 "output"
239 "overloaded"
240 "pervasive"
241 "recursor_eqns"
242 "shows"
243 "structure"
244 "type_elims"
245 "type_intros"
246 "unchecked"
247 "where"))
249 (defconst isar-keywords-control
250 '("Isabelle\\.command"
251 "ProofGeneral\\.inform_file_processed"
252 "ProofGeneral\\.inform_file_retracted"
253 "ProofGeneral\\.kill_proof"
254 "ProofGeneral\\.pr"
255 "ProofGeneral\\.process_pgip"
256 "ProofGeneral\\.restart"
257 "ProofGeneral\\.undo"
258 "cannot_undo"
259 "cd"
260 "commit"
261 "disable_pr"
262 "enable_pr"
263 "exit"
264 "init_toplevel"
265 "kill"
266 "kill_thy"
267 "linear_undo"
268 "pretty_setmargin"
269 "quit"
270 "remove_thy"
271 "undo"
272 "undos_proof"
273 "use_thy"))
275 (defconst isar-keywords-diag
276 '("ML_command"
277 "ML_val"
278 "class_deps"
279 "display_drafts"
280 "find_consts"
281 "find_theorems"
282 "full_prf"
283 "header"
284 "help"
285 "locale_deps"
286 "pr"
287 "prf"
288 "print_abbrevs"
289 "print_antiquotations"
290 "print_attributes"
291 "print_binds"
292 "print_bundles"
293 "print_cases"
294 "print_claset"
295 "print_classes"
296 "print_codesetup"
297 "print_commands"
298 "print_context"
299 "print_defn_rules"
300 "print_dependencies"
301 "print_facts"
302 "print_induct_rules"
303 "print_interps"
304 "print_locale"
305 "print_locales"
306 "print_methods"
307 "print_options"
308 "print_rules"
309 "print_simpset"
310 "print_state"
311 "print_statement"
312 "print_syntax"
313 "print_tcset"
314 "print_theorems"
315 "print_theory"
316 "print_trans_rules"
317 "prop"
318 "pwd"
319 "term"
320 "thm"
321 "thm_deps"
322 "thy_deps"
323 "typ"
324 "unused_thms"
325 "welcome"))
327 (defconst isar-keywords-theory-begin
328 '("theory"))
330 (defconst isar-keywords-theory-switch
331 '())
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"
344 "ML_file"
345 "abbreviation"
346 "attribute_setup"
347 "axiomatization"
348 "bundle"
349 "class"
350 "codatatype"
351 "code_datatype"
352 "coinductive"
353 "consts"
354 "context"
355 "datatype"
356 "declaration"
357 "declare"
358 "default_sort"
359 "definition"
360 "defs"
361 "extract"
362 "extract_type"
363 "hide_class"
364 "hide_const"
365 "hide_fact"
366 "hide_type"
367 "inductive"
368 "instantiation"
369 "judgment"
370 "lemmas"
371 "local_setup"
372 "locale"
373 "method_setup"
374 "no_notation"
375 "no_syntax"
376 "no_translations"
377 "no_type_notation"
378 "nonterminal"
379 "notation"
380 "notepad"
381 "oracle"
382 "overloading"
383 "parse_ast_translation"
384 "parse_translation"
385 "primrec"
386 "print_ast_translation"
387 "print_translation"
388 "realizability"
389 "realizers"
390 "rep_datatype"
391 "setup"
392 "simproc_setup"
393 "syntax"
394 "syntax_declaration"
395 "text"
396 "text_raw"
397 "theorems"
398 "translations"
399 "type_notation"
400 "type_synonym"
401 "typed_print_translation"
402 "typedecl"))
404 (defconst isar-keywords-theory-script
405 '("inductive_cases"))
407 (defconst isar-keywords-theory-goal
408 '("corollary"
409 "instance"
410 "interpretation"
411 "lemma"
412 "schematic_corollary"
413 "schematic_lemma"
414 "schematic_theorem"
415 "subclass"
416 "sublocale"
417 "theorem"))
419 (defconst isar-keywords-qed
420 '("\\."
421 "\\.\\."
422 "by"
423 "done"
424 "sorry"))
426 (defconst isar-keywords-qed-block
427 '("qed"))
429 (defconst isar-keywords-qed-global
430 '("oops"))
432 (defconst isar-keywords-proof-heading
433 '("sect"
434 "subsect"
435 "subsubsect"))
437 (defconst isar-keywords-proof-goal
438 '("have"
439 "hence"
440 "interpret"))
442 (defconst isar-keywords-proof-block
443 '("next"
444 "proof"))
446 (defconst isar-keywords-proof-open
447 '("{"))
449 (defconst isar-keywords-proof-close
450 '("}"))
452 (defconst isar-keywords-proof-chain
453 '("finally"
454 "from"
455 "then"
456 "ultimately"
457 "with"))
459 (defconst isar-keywords-proof-decl
460 '("ML_prf"
461 "also"
462 "include"
463 "including"
464 "let"
465 "moreover"
466 "note"
467 "txt"
468 "txt_raw"
469 "unfolding"
470 "using"
471 "write"))
473 (defconst isar-keywords-proof-asm
474 '("assume"
475 "case"
476 "def"
477 "fix"
478 "presume"))
480 (defconst isar-keywords-proof-asm-goal
481 '("guess"
482 "obtain"
483 "show"
484 "thus"))
486 (defconst isar-keywords-proof-script
487 '("apply"
488 "apply_end"
489 "back"
490 "defer"
491 "prefer"))
493 (provide 'isar-keywords)