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