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