| author | wenzelm |
| Wed, 14 Nov 2001 23:14:59 +0100 | |
| changeset 12184 | f4aaa2647fd2 |
| parent 12179 | 5b427479cc14 |
| child 12211 | 510c3eee55de |
| 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_simpset"
108 "print_syntax"
109 "print_tcset"
110 "print_theorems"
111 "print_theory"
112 "print_trans_rules"
113 "print_translation"
114 "proof"
115 "prop"
116 "pwd"
117 "qed"
118 "quit"
119 "redo"
120 "remove_thy"
121 "sect"
122 "section"
123 "setup"
124 "show"
125 "sorry"
126 "subsect"
127 "subsection"
128 "subsubsect"
129 "subsubsection"
130 "syntax"
131 "term"
132 "text"
133 "text_raw"
134 "then"
135 "theorem"
136 "theorems"
137 "theory"
138 "thm"
139 "thm_deps"
140 "thms_containing"
141 "thus"
142 "token_translation"
143 "touch_all_thys"
144 "touch_child_thys"
145 "touch_thy"
146 "translations"
147 "txt"
148 "txt_raw"
149 "typ"
150 "typed_print_translation"
151 "typedecl"
152 "types"
153 "types_code"
154 "ultimately"
155 "undo"
156 "undos_proof"
157 "update_thy"
158 "update_thy_only"
159 "use"
160 "use_thy"
161 "use_thy_only"
162 "welcome"
163 "with"
164 "{"
165 "}"))
167 (defconst isar-keywords-minor
168 '("and"
169 "assumes"
170 "binder"
171 "con_defs"
172 "concl"
173 "defines"
174 "domains"
175 "files"
176 "fixes"
177 "in"
178 "infix"
179 "infixl"
180 "infixr"
181 "intros"
182 "is"
183 "monos"
184 "notes"
185 "output"
186 "overloaded"
187 "structure"
188 "type_elims"
189 "type_intros"
190 "uses"
191 "where"))
193 (defconst isar-keywords-control
194 '("ProofGeneral\\.context_thy_only"
195 "ProofGeneral\\.inform_file_processed"
196 "ProofGeneral\\.inform_file_retracted"
197 "ProofGeneral\\.kill_proof"
198 "ProofGeneral\\.restart"
199 "ProofGeneral\\.try_context_thy_only"
200 "ProofGeneral\\.undo"
201 "cannot_undo"
202 "clear_undos"
203 "exit"
204 "init_toplevel"
205 "kill"
206 "quit"
207 "redo"
208 "undo"
209 "undos_proof"))
211 (defconst isar-keywords-diag
212 '("ML"
213 "ML_command"
214 "cd"
215 "commit"
216 "disable_pr"
217 "enable_pr"
218 "full_prf"
219 "header"
220 "kill_thy"
221 "pr"
222 "pretty_setmargin"
223 "prf"
224 "print_antiquotations"
225 "print_attributes"
226 "print_binds"
227 "print_cases"
228 "print_claset"
229 "print_commands"
230 "print_context"
231 "print_facts"
232 "print_induct_rules"
233 "print_locale"
234 "print_locales"
235 "print_methods"
236 "print_simpset"
237 "print_syntax"
238 "print_tcset"
239 "print_theorems"
240 "print_theory"
241 "print_trans_rules"
242 "prop"
243 "pwd"
244 "remove_thy"
245 "term"
246 "thm"
247 "thm_deps"
248 "thms_containing"
249 "touch_all_thys"
250 "touch_child_thys"
251 "touch_thy"
252 "typ"
253 "update_thy"
254 "update_thy_only"
255 "use"
256 "use_thy"
257 "use_thy_only"
258 "welcome"))
260 (defconst isar-keywords-theory-begin
261 '("theory"))
263 (defconst isar-keywords-theory-switch
264 '("context"))
266 (defconst isar-keywords-theory-end
267 '("end"))
269 (defconst isar-keywords-theory-heading
270 '("chapter"
271 "section"
272 "subsection"
273 "subsubsection"))
275 (defconst isar-keywords-theory-decl
276 '("ML_setup"
277 "arities"
278 "axclass"
279 "axioms"
280 "classes"
281 "classrel"
282 "codatatype"
283 "coinductive"
284 "constdefs"
285 "consts"
286 "consts_code"
287 "datatype"
288 "defaultsort"
289 "defs"
290 "generate_code"
291 "global"
292 "hide"
293 "inductive"
294 "judgment"
295 "lemmas"
296 "local"
297 "locale"
298 "method_setup"
299 "nonterminals"
300 "oracle"
301 "parse_ast_translation"
302 "parse_translation"
303 "primrec"
304 "print_ast_translation"
305 "print_translation"
306 "setup"
307 "syntax"
308 "text"
309 "text_raw"
310 "theorems"
311 "token_translation"
312 "translations"
313 "typed_print_translation"
314 "typedecl"
315 "types"
316 "types_code"))
318 (defconst isar-keywords-theory-script
319 '("declare"
320 "inductive_cases"))
322 (defconst isar-keywords-theory-goal
323 '("corollary"
324 "instance"
325 "lemma"
326 "theorem"))
328 (defconst isar-keywords-qed
329 '("\\."
330 "\\.\\."
331 "by"
332 "done"
333 "sorry"))
335 (defconst isar-keywords-qed-block
336 '("qed"))
338 (defconst isar-keywords-qed-global
339 '("oops"))
341 (defconst isar-keywords-proof-heading
342 '("sect"
343 "subsect"
344 "subsubsect"))
346 (defconst isar-keywords-proof-goal
347 '("have"
348 "hence"
349 "show"
350 "thus"))
352 (defconst isar-keywords-proof-block
353 '("next"
354 "proof"))
356 (defconst isar-keywords-proof-open
357 '("{"))
359 (defconst isar-keywords-proof-close
360 '("}"))
362 (defconst isar-keywords-proof-chain
363 '("finally"
364 "from"
365 "then"
366 "ultimately"
367 "with"))
369 (defconst isar-keywords-proof-decl
370 '("also"
371 "let"
372 "moreover"
373 "note"
374 "txt"
375 "txt_raw"))
377 (defconst isar-keywords-proof-asm
378 '("assume"
379 "case"
380 "def"
381 "fix"
382 "presume"))
384 (defconst isar-keywords-proof-asm-goal
385 '("obtain"))
387 (defconst isar-keywords-proof-script
388 '("apply"
389 "apply_end"
390 "back"
391 "defer"
392 "prefer"))
394 (provide 'isar-keywords)