| author | wenzelm |
| Mon, 25 Feb 2002 20:33:40 +0100 | |
| changeset 12935 | d697091d1591 |
| parent 12926 | cd0dd6e0bf5c |
| child 12954 | 850609c057e2 |
| 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 "using"
165 "welcome"
166 "with"
167 "{"
168 "}"))
170 (defconst isar-keywords-minor
171 '("and"
172 "assumes"
173 "binder"
174 "case_eqns"
175 "con_defs"
176 "concl"
177 "defines"
178 "domains"
179 "elimination"
180 "files"
181 "fixes"
182 "in"
183 "induction"
184 "infix"
185 "infixl"
186 "infixr"
187 "intros"
188 "is"
189 "monos"
190 "notes"
191 "output"
192 "overloaded"
193 "recursor_eqns"
194 "shows"
195 "structure"
196 "type_elims"
197 "type_intros"
198 "uses"
199 "where"))
201 (defconst isar-keywords-control
202 '("ProofGeneral\\.context_thy_only"
203 "ProofGeneral\\.inform_file_processed"
204 "ProofGeneral\\.inform_file_retracted"
205 "ProofGeneral\\.kill_proof"
206 "ProofGeneral\\.restart"
207 "ProofGeneral\\.try_context_thy_only"
208 "ProofGeneral\\.undo"
209 "cannot_undo"
210 "clear_undos"
211 "exit"
212 "init_toplevel"
213 "kill"
214 "quit"
215 "redo"
216 "undo"
217 "undos_proof"))
219 (defconst isar-keywords-diag
220 '("ML"
221 "ML_command"
222 "cd"
223 "commit"
224 "disable_pr"
225 "enable_pr"
226 "full_prf"
227 "header"
228 "kill_thy"
229 "pr"
230 "pretty_setmargin"
231 "prf"
232 "print_antiquotations"
233 "print_attributes"
234 "print_binds"
235 "print_cases"
236 "print_claset"
237 "print_commands"
238 "print_context"
239 "print_facts"
240 "print_induct_rules"
241 "print_locale"
242 "print_locales"
243 "print_methods"
244 "print_rules"
245 "print_simpset"
246 "print_syntax"
247 "print_tcset"
248 "print_theorems"
249 "print_theory"
250 "print_trans_rules"
251 "prop"
252 "pwd"
253 "remove_thy"
254 "term"
255 "thm"
256 "thm_deps"
257 "thms_containing"
258 "touch_all_thys"
259 "touch_child_thys"
260 "touch_thy"
261 "typ"
262 "update_thy"
263 "update_thy_only"
264 "use"
265 "use_thy"
266 "use_thy_only"
267 "welcome"))
269 (defconst isar-keywords-theory-begin
270 '("theory"))
272 (defconst isar-keywords-theory-switch
273 '("context"))
275 (defconst isar-keywords-theory-end
276 '("end"))
278 (defconst isar-keywords-theory-heading
279 '("chapter"
280 "section"
281 "subsection"
282 "subsubsection"))
284 (defconst isar-keywords-theory-decl
285 '("ML_setup"
286 "arities"
287 "axclass"
288 "axioms"
289 "classes"
290 "classrel"
291 "codatatype"
292 "coinductive"
293 "constdefs"
294 "consts"
295 "consts_code"
296 "datatype"
297 "defaultsort"
298 "defs"
299 "generate_code"
300 "global"
301 "hide"
302 "inductive"
303 "judgment"
304 "lemmas"
305 "local"
306 "locale"
307 "method_setup"
308 "nonterminals"
309 "oracle"
310 "parse_ast_translation"
311 "parse_translation"
312 "primrec"
313 "print_ast_translation"
314 "print_translation"
315 "rep_datatype"
316 "setup"
317 "syntax"
318 "text"
319 "text_raw"
320 "theorems"
321 "token_translation"
322 "translations"
323 "typed_print_translation"
324 "typedecl"
325 "types"
326 "types_code"))
328 (defconst isar-keywords-theory-script
329 '("declare"
330 "inductive_cases"))
332 (defconst isar-keywords-theory-goal
333 '("corollary"
334 "instance"
335 "lemma"
336 "theorem"))
338 (defconst isar-keywords-qed
339 '("\\."
340 "\\.\\."
341 "by"
342 "done"
343 "sorry"))
345 (defconst isar-keywords-qed-block
346 '("qed"))
348 (defconst isar-keywords-qed-global
349 '("oops"))
351 (defconst isar-keywords-proof-heading
352 '("sect"
353 "subsect"
354 "subsubsect"))
356 (defconst isar-keywords-proof-goal
357 '("have"
358 "hence"
359 "show"
360 "thus"))
362 (defconst isar-keywords-proof-block
363 '("next"
364 "proof"))
366 (defconst isar-keywords-proof-open
367 '("{"))
369 (defconst isar-keywords-proof-close
370 '("}"))
372 (defconst isar-keywords-proof-chain
373 '("finally"
374 "from"
375 "then"
376 "ultimately"
377 "with"))
379 (defconst isar-keywords-proof-decl
380 '("also"
381 "let"
382 "moreover"
383 "note"
384 "txt"
385 "txt_raw"
386 "using"))
388 (defconst isar-keywords-proof-asm
389 '("assume"
390 "case"
391 "def"
392 "fix"
393 "presume"))
395 (defconst isar-keywords-proof-asm-goal
396 '("obtain"))
398 (defconst isar-keywords-proof-script
399 '("apply"
400 "apply_end"
401 "back"
402 "defer"
403 "prefer"))
405 (provide 'isar-keywords)