1 ;; |
|
2 ;; Keyword classification tables for Isabelle/Isar. |
|
3 ;; Generated from Pure + ZF. |
|
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** |
|
5 ;; |
|
6 |
|
7 (defconst isar-keywords-major |
|
8 '("\\." |
|
9 "\\.\\." |
|
10 "Isabelle\\.command" |
|
11 "ML" |
|
12 "ML_command" |
|
13 "ML_file" |
|
14 "ML_prf" |
|
15 "ML_val" |
|
16 "ProofGeneral\\.inform_file_processed" |
|
17 "ProofGeneral\\.inform_file_retracted" |
|
18 "ProofGeneral\\.kill_proof" |
|
19 "ProofGeneral\\.pr" |
|
20 "ProofGeneral\\.process_pgip" |
|
21 "ProofGeneral\\.restart" |
|
22 "ProofGeneral\\.undo" |
|
23 "SML_export" |
|
24 "SML_file" |
|
25 "SML_import" |
|
26 "abbreviation" |
|
27 "also" |
|
28 "apply" |
|
29 "apply_end" |
|
30 "assume" |
|
31 "attribute_setup" |
|
32 "axiomatization" |
|
33 "back" |
|
34 "bundle" |
|
35 "by" |
|
36 "cannot_undo" |
|
37 "case" |
|
38 "chapter" |
|
39 "class" |
|
40 "class_deps" |
|
41 "codatatype" |
|
42 "code_datatype" |
|
43 "coinductive" |
|
44 "commit" |
|
45 "consts" |
|
46 "context" |
|
47 "corollary" |
|
48 "datatype" |
|
49 "declaration" |
|
50 "declare" |
|
51 "def" |
|
52 "default_sort" |
|
53 "defer" |
|
54 "definition" |
|
55 "defs" |
|
56 "disable_pr" |
|
57 "display_drafts" |
|
58 "done" |
|
59 "enable_pr" |
|
60 "end" |
|
61 "exit" |
|
62 "extract" |
|
63 "extract_type" |
|
64 "finally" |
|
65 "find_consts" |
|
66 "find_theorems" |
|
67 "fix" |
|
68 "from" |
|
69 "full_prf" |
|
70 "guess" |
|
71 "have" |
|
72 "header" |
|
73 "help" |
|
74 "hence" |
|
75 "hide_class" |
|
76 "hide_const" |
|
77 "hide_fact" |
|
78 "hide_type" |
|
79 "include" |
|
80 "including" |
|
81 "inductive" |
|
82 "inductive_cases" |
|
83 "init_toplevel" |
|
84 "instance" |
|
85 "instantiation" |
|
86 "interpret" |
|
87 "interpretation" |
|
88 "judgment" |
|
89 "kill" |
|
90 "kill_thy" |
|
91 "lemma" |
|
92 "lemmas" |
|
93 "let" |
|
94 "linear_undo" |
|
95 "local_setup" |
|
96 "locale" |
|
97 "locale_deps" |
|
98 "method_setup" |
|
99 "moreover" |
|
100 "named_theorems" |
|
101 "next" |
|
102 "no_notation" |
|
103 "no_syntax" |
|
104 "no_translations" |
|
105 "no_type_notation" |
|
106 "nonterminal" |
|
107 "notation" |
|
108 "note" |
|
109 "notepad" |
|
110 "obtain" |
|
111 "oops" |
|
112 "oracle" |
|
113 "overloading" |
|
114 "parse_ast_translation" |
|
115 "parse_translation" |
|
116 "pr" |
|
117 "prefer" |
|
118 "presume" |
|
119 "pretty_setmargin" |
|
120 "prf" |
|
121 "primrec" |
|
122 "print_ML_antiquotations" |
|
123 "print_abbrevs" |
|
124 "print_antiquotations" |
|
125 "print_ast_translation" |
|
126 "print_attributes" |
|
127 "print_binds" |
|
128 "print_bundles" |
|
129 "print_cases" |
|
130 "print_claset" |
|
131 "print_classes" |
|
132 "print_codesetup" |
|
133 "print_commands" |
|
134 "print_context" |
|
135 "print_defn_rules" |
|
136 "print_dependencies" |
|
137 "print_facts" |
|
138 "print_induct_rules" |
|
139 "print_interps" |
|
140 "print_locale" |
|
141 "print_locales" |
|
142 "print_methods" |
|
143 "print_options" |
|
144 "print_rules" |
|
145 "print_simpset" |
|
146 "print_state" |
|
147 "print_statement" |
|
148 "print_syntax" |
|
149 "print_tcset" |
|
150 "print_term_bindings" |
|
151 "print_theorems" |
|
152 "print_theory" |
|
153 "print_trans_rules" |
|
154 "print_translation" |
|
155 "proof" |
|
156 "prop" |
|
157 "qed" |
|
158 "quit" |
|
159 "realizability" |
|
160 "realizers" |
|
161 "remove_thy" |
|
162 "rep_datatype" |
|
163 "schematic_corollary" |
|
164 "schematic_lemma" |
|
165 "schematic_theorem" |
|
166 "sect" |
|
167 "section" |
|
168 "setup" |
|
169 "show" |
|
170 "simproc_setup" |
|
171 "sorry" |
|
172 "subclass" |
|
173 "sublocale" |
|
174 "subsect" |
|
175 "subsection" |
|
176 "subsubsect" |
|
177 "subsubsection" |
|
178 "syntax" |
|
179 "syntax_declaration" |
|
180 "term" |
|
181 "text" |
|
182 "text_raw" |
|
183 "then" |
|
184 "theorem" |
|
185 "theorems" |
|
186 "theory" |
|
187 "thm" |
|
188 "thm_deps" |
|
189 "thus" |
|
190 "thy_deps" |
|
191 "translations" |
|
192 "txt" |
|
193 "txt_raw" |
|
194 "typ" |
|
195 "type_notation" |
|
196 "type_synonym" |
|
197 "typed_print_translation" |
|
198 "typedecl" |
|
199 "ultimately" |
|
200 "undo" |
|
201 "undos_proof" |
|
202 "unfolding" |
|
203 "unused_thms" |
|
204 "use_thy" |
|
205 "using" |
|
206 "welcome" |
|
207 "with" |
|
208 "write" |
|
209 "{" |
|
210 "}")) |
|
211 |
|
212 (defconst isar-keywords-minor |
|
213 '("and" |
|
214 "assumes" |
|
215 "attach" |
|
216 "begin" |
|
217 "binder" |
|
218 "case_eqns" |
|
219 "con_defs" |
|
220 "constrains" |
|
221 "defines" |
|
222 "domains" |
|
223 "elimination" |
|
224 "fixes" |
|
225 "for" |
|
226 "identifier" |
|
227 "if" |
|
228 "imports" |
|
229 "in" |
|
230 "includes" |
|
231 "induction" |
|
232 "infix" |
|
233 "infixl" |
|
234 "infixr" |
|
235 "intros" |
|
236 "is" |
|
237 "keywords" |
|
238 "monos" |
|
239 "notes" |
|
240 "obtains" |
|
241 "open" |
|
242 "output" |
|
243 "overloaded" |
|
244 "pervasive" |
|
245 "recursor_eqns" |
|
246 "shows" |
|
247 "structure" |
|
248 "type_elims" |
|
249 "type_intros" |
|
250 "unchecked" |
|
251 "where")) |
|
252 |
|
253 (defconst isar-keywords-control |
|
254 '("Isabelle\\.command" |
|
255 "ProofGeneral\\.inform_file_processed" |
|
256 "ProofGeneral\\.inform_file_retracted" |
|
257 "ProofGeneral\\.kill_proof" |
|
258 "ProofGeneral\\.pr" |
|
259 "ProofGeneral\\.process_pgip" |
|
260 "ProofGeneral\\.restart" |
|
261 "ProofGeneral\\.undo" |
|
262 "cannot_undo" |
|
263 "commit" |
|
264 "disable_pr" |
|
265 "enable_pr" |
|
266 "exit" |
|
267 "init_toplevel" |
|
268 "kill" |
|
269 "kill_thy" |
|
270 "linear_undo" |
|
271 "pretty_setmargin" |
|
272 "quit" |
|
273 "remove_thy" |
|
274 "undo" |
|
275 "undos_proof" |
|
276 "use_thy")) |
|
277 |
|
278 (defconst isar-keywords-diag |
|
279 '("ML_command" |
|
280 "ML_val" |
|
281 "class_deps" |
|
282 "display_drafts" |
|
283 "find_consts" |
|
284 "find_theorems" |
|
285 "full_prf" |
|
286 "header" |
|
287 "help" |
|
288 "locale_deps" |
|
289 "pr" |
|
290 "prf" |
|
291 "print_ML_antiquotations" |
|
292 "print_abbrevs" |
|
293 "print_antiquotations" |
|
294 "print_attributes" |
|
295 "print_binds" |
|
296 "print_bundles" |
|
297 "print_cases" |
|
298 "print_claset" |
|
299 "print_classes" |
|
300 "print_codesetup" |
|
301 "print_commands" |
|
302 "print_context" |
|
303 "print_defn_rules" |
|
304 "print_dependencies" |
|
305 "print_facts" |
|
306 "print_induct_rules" |
|
307 "print_interps" |
|
308 "print_locale" |
|
309 "print_locales" |
|
310 "print_methods" |
|
311 "print_options" |
|
312 "print_rules" |
|
313 "print_simpset" |
|
314 "print_state" |
|
315 "print_statement" |
|
316 "print_syntax" |
|
317 "print_tcset" |
|
318 "print_term_bindings" |
|
319 "print_theorems" |
|
320 "print_theory" |
|
321 "print_trans_rules" |
|
322 "prop" |
|
323 "term" |
|
324 "thm" |
|
325 "thm_deps" |
|
326 "thy_deps" |
|
327 "typ" |
|
328 "unused_thms" |
|
329 "welcome")) |
|
330 |
|
331 (defconst isar-keywords-theory-begin |
|
332 '("theory")) |
|
333 |
|
334 (defconst isar-keywords-theory-switch |
|
335 '()) |
|
336 |
|
337 (defconst isar-keywords-theory-end |
|
338 '("end")) |
|
339 |
|
340 (defconst isar-keywords-theory-heading |
|
341 '("chapter" |
|
342 "section" |
|
343 "subsection" |
|
344 "subsubsection")) |
|
345 |
|
346 (defconst isar-keywords-theory-decl |
|
347 '("ML" |
|
348 "ML_file" |
|
349 "SML_export" |
|
350 "SML_file" |
|
351 "SML_import" |
|
352 "abbreviation" |
|
353 "attribute_setup" |
|
354 "axiomatization" |
|
355 "bundle" |
|
356 "class" |
|
357 "codatatype" |
|
358 "code_datatype" |
|
359 "coinductive" |
|
360 "consts" |
|
361 "context" |
|
362 "datatype" |
|
363 "declaration" |
|
364 "declare" |
|
365 "default_sort" |
|
366 "definition" |
|
367 "defs" |
|
368 "extract" |
|
369 "extract_type" |
|
370 "hide_class" |
|
371 "hide_const" |
|
372 "hide_fact" |
|
373 "hide_type" |
|
374 "inductive" |
|
375 "inductive_cases" |
|
376 "instantiation" |
|
377 "judgment" |
|
378 "lemmas" |
|
379 "local_setup" |
|
380 "locale" |
|
381 "method_setup" |
|
382 "named_theorems" |
|
383 "no_notation" |
|
384 "no_syntax" |
|
385 "no_translations" |
|
386 "no_type_notation" |
|
387 "nonterminal" |
|
388 "notation" |
|
389 "notepad" |
|
390 "oracle" |
|
391 "overloading" |
|
392 "parse_ast_translation" |
|
393 "parse_translation" |
|
394 "primrec" |
|
395 "print_ast_translation" |
|
396 "print_translation" |
|
397 "realizability" |
|
398 "realizers" |
|
399 "rep_datatype" |
|
400 "setup" |
|
401 "simproc_setup" |
|
402 "syntax" |
|
403 "syntax_declaration" |
|
404 "text" |
|
405 "text_raw" |
|
406 "theorems" |
|
407 "translations" |
|
408 "type_notation" |
|
409 "type_synonym" |
|
410 "typed_print_translation" |
|
411 "typedecl")) |
|
412 |
|
413 (defconst isar-keywords-theory-script |
|
414 '()) |
|
415 |
|
416 (defconst isar-keywords-theory-goal |
|
417 '("corollary" |
|
418 "instance" |
|
419 "interpretation" |
|
420 "lemma" |
|
421 "schematic_corollary" |
|
422 "schematic_lemma" |
|
423 "schematic_theorem" |
|
424 "subclass" |
|
425 "sublocale" |
|
426 "theorem")) |
|
427 |
|
428 (defconst isar-keywords-qed |
|
429 '("\\." |
|
430 "\\.\\." |
|
431 "by" |
|
432 "done" |
|
433 "sorry")) |
|
434 |
|
435 (defconst isar-keywords-qed-block |
|
436 '("qed")) |
|
437 |
|
438 (defconst isar-keywords-qed-global |
|
439 '("oops")) |
|
440 |
|
441 (defconst isar-keywords-proof-heading |
|
442 '("sect" |
|
443 "subsect" |
|
444 "subsubsect")) |
|
445 |
|
446 (defconst isar-keywords-proof-goal |
|
447 '("have" |
|
448 "hence" |
|
449 "interpret")) |
|
450 |
|
451 (defconst isar-keywords-proof-block |
|
452 '("next" |
|
453 "proof")) |
|
454 |
|
455 (defconst isar-keywords-proof-open |
|
456 '("{")) |
|
457 |
|
458 (defconst isar-keywords-proof-close |
|
459 '("}")) |
|
460 |
|
461 (defconst isar-keywords-proof-chain |
|
462 '("finally" |
|
463 "from" |
|
464 "then" |
|
465 "ultimately" |
|
466 "with")) |
|
467 |
|
468 (defconst isar-keywords-proof-decl |
|
469 '("ML_prf" |
|
470 "also" |
|
471 "include" |
|
472 "including" |
|
473 "let" |
|
474 "moreover" |
|
475 "note" |
|
476 "txt" |
|
477 "txt_raw" |
|
478 "unfolding" |
|
479 "using" |
|
480 "write")) |
|
481 |
|
482 (defconst isar-keywords-proof-asm |
|
483 '("assume" |
|
484 "case" |
|
485 "def" |
|
486 "fix" |
|
487 "presume")) |
|
488 |
|
489 (defconst isar-keywords-proof-asm-goal |
|
490 '("guess" |
|
491 "obtain" |
|
492 "show" |
|
493 "thus")) |
|
494 |
|
495 (defconst isar-keywords-proof-script |
|
496 '("apply" |
|
497 "apply_end" |
|
498 "back" |
|
499 "defer" |
|
500 "prefer")) |
|
501 |
|
502 (provide 'isar-keywords) |
|