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