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