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