|
1 ;; |
|
2 ;; Keyword classification tables for Isabelle/Isar. |
|
3 ;; Generated from HOL-Nominal-Quot + HOL-Nominal + HOL + Pure-ProofGeneral + Pure. |
|
4 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** |
|
5 ;; |
|
6 |
|
7 (defconst isar-keywords-major |
|
8 '("\\." |
|
9 "\\.\\." |
|
10 "Isabelle\\.command" |
|
11 "Isar\\.begin_document" |
|
12 "Isar\\.define_command" |
|
13 "Isar\\.edit_document" |
|
14 "Isar\\.end_document" |
|
15 "ML" |
|
16 "ML_command" |
|
17 "ML_prf" |
|
18 "ML_val" |
|
19 "ProofGeneral\\.inform_file_processed" |
|
20 "ProofGeneral\\.inform_file_retracted" |
|
21 "ProofGeneral\\.kill_proof" |
|
22 "ProofGeneral\\.pr" |
|
23 "ProofGeneral\\.process_pgip" |
|
24 "ProofGeneral\\.restart" |
|
25 "ProofGeneral\\.undo" |
|
26 "abbreviation" |
|
27 "also" |
|
28 "apply" |
|
29 "apply_end" |
|
30 "arities" |
|
31 "assume" |
|
32 "atom_decl" |
|
33 "atp_info" |
|
34 "atp_kill" |
|
35 "atp_messages" |
|
36 "atp_minimize" |
|
37 "attribute_setup" |
|
38 "ax_specification" |
|
39 "axclass" |
|
40 "axiomatization" |
|
41 "axioms" |
|
42 "back" |
|
43 "by" |
|
44 "cannot_undo" |
|
45 "case" |
|
46 "cd" |
|
47 "chapter" |
|
48 "class" |
|
49 "class_deps" |
|
50 "classes" |
|
51 "classrel" |
|
52 "code_abort" |
|
53 "code_class" |
|
54 "code_const" |
|
55 "code_datatype" |
|
56 "code_deps" |
|
57 "code_include" |
|
58 "code_instance" |
|
59 "code_library" |
|
60 "code_module" |
|
61 "code_modulename" |
|
62 "code_monad" |
|
63 "code_pred" |
|
64 "code_reflect" |
|
65 "code_reserved" |
|
66 "code_thms" |
|
67 "code_type" |
|
68 "coinductive" |
|
69 "coinductive_set" |
|
70 "commit" |
|
71 "constdefs" |
|
72 "consts" |
|
73 "consts_code" |
|
74 "context" |
|
75 "corollary" |
|
76 "datatype" |
|
77 "declaration" |
|
78 "declare" |
|
79 "def" |
|
80 "default_sort" |
|
81 "defer" |
|
82 "defer_recdef" |
|
83 "definition" |
|
84 "defs" |
|
85 "disable_pr" |
|
86 "display_drafts" |
|
87 "done" |
|
88 "enable_pr" |
|
89 "end" |
|
90 "equivariance" |
|
91 "exit" |
|
92 "export_code" |
|
93 "extract" |
|
94 "extract_type" |
|
95 "finalconsts" |
|
96 "finally" |
|
97 "find_consts" |
|
98 "find_theorems" |
|
99 "fix" |
|
100 "from" |
|
101 "full_prf" |
|
102 "fun" |
|
103 "function" |
|
104 "global" |
|
105 "guess" |
|
106 "have" |
|
107 "header" |
|
108 "help" |
|
109 "hence" |
|
110 "hide_class" |
|
111 "hide_const" |
|
112 "hide_fact" |
|
113 "hide_type" |
|
114 "inductive" |
|
115 "inductive_cases" |
|
116 "inductive_set" |
|
117 "init_toplevel" |
|
118 "instance" |
|
119 "instantiation" |
|
120 "interpret" |
|
121 "interpretation" |
|
122 "judgment" |
|
123 "kill" |
|
124 "kill_thy" |
|
125 "lemma" |
|
126 "lemmas" |
|
127 "let" |
|
128 "linear_undo" |
|
129 "local" |
|
130 "local_setup" |
|
131 "locale" |
|
132 "method_setup" |
|
133 "moreover" |
|
134 "next" |
|
135 "nitpick" |
|
136 "nitpick_params" |
|
137 "no_notation" |
|
138 "no_syntax" |
|
139 "no_translations" |
|
140 "nominal_datatype" |
|
141 "nominal_inductive" |
|
142 "nominal_inductive2" |
|
143 "nominal_primrec" |
|
144 "nonterminals" |
|
145 "normal_form" |
|
146 "notation" |
|
147 "note" |
|
148 "obtain" |
|
149 "oops" |
|
150 "oracle" |
|
151 "overloading" |
|
152 "parse_ast_translation" |
|
153 "parse_translation" |
|
154 "pr" |
|
155 "prefer" |
|
156 "presume" |
|
157 "pretty_setmargin" |
|
158 "prf" |
|
159 "primrec" |
|
160 "print_abbrevs" |
|
161 "print_antiquotations" |
|
162 "print_ast_translation" |
|
163 "print_atps" |
|
164 "print_attributes" |
|
165 "print_binds" |
|
166 "print_cases" |
|
167 "print_claset" |
|
168 "print_classes" |
|
169 "print_codeproc" |
|
170 "print_codesetup" |
|
171 "print_commands" |
|
172 "print_configs" |
|
173 "print_context" |
|
174 "print_drafts" |
|
175 "print_facts" |
|
176 "print_induct_rules" |
|
177 "print_interps" |
|
178 "print_locale" |
|
179 "print_locales" |
|
180 "print_maps" |
|
181 "print_methods" |
|
182 "print_orders" |
|
183 "print_quotconsts" |
|
184 "print_quotients" |
|
185 "print_rules" |
|
186 "print_simpset" |
|
187 "print_statement" |
|
188 "print_syntax" |
|
189 "print_theorems" |
|
190 "print_theory" |
|
191 "print_trans_rules" |
|
192 "print_translation" |
|
193 "proof" |
|
194 "prop" |
|
195 "prove" |
|
196 "pwd" |
|
197 "qed" |
|
198 "quickcheck" |
|
199 "quickcheck_params" |
|
200 "quit" |
|
201 "quotient_definition" |
|
202 "quotient_type" |
|
203 "realizability" |
|
204 "realizers" |
|
205 "recdef" |
|
206 "recdef_tc" |
|
207 "record" |
|
208 "refute" |
|
209 "refute_params" |
|
210 "remove_thy" |
|
211 "rep_datatype" |
|
212 "repdef" |
|
213 "schematic_corollary" |
|
214 "schematic_lemma" |
|
215 "schematic_theorem" |
|
216 "sect" |
|
217 "section" |
|
218 "setup" |
|
219 "show" |
|
220 "simproc_setup" |
|
221 "sledgehammer" |
|
222 "sledgehammer_params" |
|
223 "smt_status" |
|
224 "sorry" |
|
225 "specification" |
|
226 "subclass" |
|
227 "sublocale" |
|
228 "subsect" |
|
229 "subsection" |
|
230 "subsubsect" |
|
231 "subsubsection" |
|
232 "syntax" |
|
233 "term" |
|
234 "termination" |
|
235 "text" |
|
236 "text_raw" |
|
237 "then" |
|
238 "theorem" |
|
239 "theorems" |
|
240 "theory" |
|
241 "thm" |
|
242 "thm_deps" |
|
243 "thus" |
|
244 "thy_deps" |
|
245 "touch_thy" |
|
246 "translations" |
|
247 "txt" |
|
248 "txt_raw" |
|
249 "typ" |
|
250 "typed_print_translation" |
|
251 "typedecl" |
|
252 "typedef" |
|
253 "types" |
|
254 "types_code" |
|
255 "ultimately" |
|
256 "undo" |
|
257 "undos_proof" |
|
258 "unfolding" |
|
259 "unused_thms" |
|
260 "use" |
|
261 "use_thy" |
|
262 "using" |
|
263 "value" |
|
264 "values" |
|
265 "welcome" |
|
266 "with" |
|
267 "{" |
|
268 "}")) |
|
269 |
|
270 (defconst isar-keywords-minor |
|
271 '("advanced" |
|
272 "and" |
|
273 "as" |
|
274 "assumes" |
|
275 "attach" |
|
276 "avoids" |
|
277 "begin" |
|
278 "binder" |
|
279 "congs" |
|
280 "constrains" |
|
281 "contains" |
|
282 "defines" |
|
283 "file" |
|
284 "fixes" |
|
285 "for" |
|
286 "hints" |
|
287 "identifier" |
|
288 "if" |
|
289 "imports" |
|
290 "in" |
|
291 "infix" |
|
292 "infixl" |
|
293 "infixr" |
|
294 "is" |
|
295 "module_name" |
|
296 "monos" |
|
297 "morphisms" |
|
298 "notes" |
|
299 "obtains" |
|
300 "open" |
|
301 "output" |
|
302 "overloaded" |
|
303 "permissive" |
|
304 "pervasive" |
|
305 "shows" |
|
306 "structure" |
|
307 "unchecked" |
|
308 "uses" |
|
309 "where")) |
|
310 |
|
311 (defconst isar-keywords-control |
|
312 '("Isabelle\\.command" |
|
313 "Isar\\.begin_document" |
|
314 "Isar\\.define_command" |
|
315 "Isar\\.edit_document" |
|
316 "Isar\\.end_document" |
|
317 "ProofGeneral\\.inform_file_processed" |
|
318 "ProofGeneral\\.inform_file_retracted" |
|
319 "ProofGeneral\\.kill_proof" |
|
320 "ProofGeneral\\.process_pgip" |
|
321 "ProofGeneral\\.restart" |
|
322 "ProofGeneral\\.undo" |
|
323 "cannot_undo" |
|
324 "exit" |
|
325 "init_toplevel" |
|
326 "kill" |
|
327 "linear_undo" |
|
328 "quit" |
|
329 "undo" |
|
330 "undos_proof")) |
|
331 |
|
332 (defconst isar-keywords-diag |
|
333 '("ML_command" |
|
334 "ML_val" |
|
335 "ProofGeneral\\.pr" |
|
336 "atp_info" |
|
337 "atp_kill" |
|
338 "atp_messages" |
|
339 "atp_minimize" |
|
340 "cd" |
|
341 "class_deps" |
|
342 "code_deps" |
|
343 "code_thms" |
|
344 "commit" |
|
345 "disable_pr" |
|
346 "display_drafts" |
|
347 "enable_pr" |
|
348 "export_code" |
|
349 "find_consts" |
|
350 "find_theorems" |
|
351 "full_prf" |
|
352 "header" |
|
353 "help" |
|
354 "kill_thy" |
|
355 "nitpick" |
|
356 "normal_form" |
|
357 "pr" |
|
358 "pretty_setmargin" |
|
359 "prf" |
|
360 "print_abbrevs" |
|
361 "print_antiquotations" |
|
362 "print_atps" |
|
363 "print_attributes" |
|
364 "print_binds" |
|
365 "print_cases" |
|
366 "print_claset" |
|
367 "print_classes" |
|
368 "print_codeproc" |
|
369 "print_codesetup" |
|
370 "print_commands" |
|
371 "print_configs" |
|
372 "print_context" |
|
373 "print_drafts" |
|
374 "print_facts" |
|
375 "print_induct_rules" |
|
376 "print_interps" |
|
377 "print_locale" |
|
378 "print_locales" |
|
379 "print_maps" |
|
380 "print_methods" |
|
381 "print_orders" |
|
382 "print_quotconsts" |
|
383 "print_quotients" |
|
384 "print_rules" |
|
385 "print_simpset" |
|
386 "print_statement" |
|
387 "print_syntax" |
|
388 "print_theorems" |
|
389 "print_theory" |
|
390 "print_trans_rules" |
|
391 "prop" |
|
392 "pwd" |
|
393 "quickcheck" |
|
394 "refute" |
|
395 "remove_thy" |
|
396 "sledgehammer" |
|
397 "term" |
|
398 "thm" |
|
399 "thm_deps" |
|
400 "thy_deps" |
|
401 "touch_thy" |
|
402 "typ" |
|
403 "unused_thms" |
|
404 "use_thy" |
|
405 "value" |
|
406 "values" |
|
407 "welcome")) |
|
408 |
|
409 (defconst isar-keywords-theory-begin |
|
410 '("theory")) |
|
411 |
|
412 (defconst isar-keywords-theory-switch |
|
413 '()) |
|
414 |
|
415 (defconst isar-keywords-theory-end |
|
416 '("end")) |
|
417 |
|
418 (defconst isar-keywords-theory-heading |
|
419 '("chapter" |
|
420 "section" |
|
421 "subsection" |
|
422 "subsubsection")) |
|
423 |
|
424 (defconst isar-keywords-theory-decl |
|
425 '("ML" |
|
426 "abbreviation" |
|
427 "arities" |
|
428 "atom_decl" |
|
429 "attribute_setup" |
|
430 "axclass" |
|
431 "axiomatization" |
|
432 "axioms" |
|
433 "class" |
|
434 "classes" |
|
435 "classrel" |
|
436 "code_abort" |
|
437 "code_class" |
|
438 "code_const" |
|
439 "code_datatype" |
|
440 "code_include" |
|
441 "code_instance" |
|
442 "code_library" |
|
443 "code_module" |
|
444 "code_modulename" |
|
445 "code_monad" |
|
446 "code_reflect" |
|
447 "code_reserved" |
|
448 "code_type" |
|
449 "coinductive" |
|
450 "coinductive_set" |
|
451 "constdefs" |
|
452 "consts" |
|
453 "consts_code" |
|
454 "context" |
|
455 "datatype" |
|
456 "declaration" |
|
457 "declare" |
|
458 "defaultsort" |
|
459 "defer_recdef" |
|
460 "definition" |
|
461 "defs" |
|
462 "equivariance" |
|
463 "extract" |
|
464 "extract_type" |
|
465 "finalconsts" |
|
466 "fun" |
|
467 "global" |
|
468 "hide_class" |
|
469 "hide_const" |
|
470 "hide_fact" |
|
471 "hide_type" |
|
472 "inductive" |
|
473 "inductive_set" |
|
474 "instantiation" |
|
475 "judgment" |
|
476 "lemmas" |
|
477 "local" |
|
478 "local_setup" |
|
479 "locale" |
|
480 "method_setup" |
|
481 "nitpick_params" |
|
482 "no_notation" |
|
483 "no_syntax" |
|
484 "no_translations" |
|
485 "nominal_datatype" |
|
486 "nonterminals" |
|
487 "notation" |
|
488 "oracle" |
|
489 "overloading" |
|
490 "parse_ast_translation" |
|
491 "parse_translation" |
|
492 "primrec" |
|
493 "print_ast_translation" |
|
494 "print_translation" |
|
495 "quickcheck_params" |
|
496 "quotient_definition" |
|
497 "realizability" |
|
498 "realizers" |
|
499 "recdef" |
|
500 "record" |
|
501 "refute_params" |
|
502 "setup" |
|
503 "simproc_setup" |
|
504 "sledgehammer_params" |
|
505 "statespace" |
|
506 "syntax" |
|
507 "text" |
|
508 "text_raw" |
|
509 "theorems" |
|
510 "translations" |
|
511 "typed_print_translation" |
|
512 "typedecl" |
|
513 "types" |
|
514 "types_code" |
|
515 "use")) |
|
516 |
|
517 (defconst isar-keywords-theory-script |
|
518 '("inductive_cases")) |
|
519 |
|
520 (defconst isar-keywords-theory-goal |
|
521 '("ax_specification" |
|
522 "code_pred" |
|
523 "corollary" |
|
524 "function" |
|
525 "instance" |
|
526 "interpretation" |
|
527 "lemma" |
|
528 "nominal_inductive" |
|
529 "nominal_inductive2" |
|
530 "nominal_primrec" |
|
531 "prove" |
|
532 "quotient_type" |
|
533 "recdef_tc" |
|
534 "rep_datatype" |
|
535 "schematic_corollary" |
|
536 "schematic_lemma" |
|
537 "schematic_theorem" |
|
538 "specification" |
|
539 "subclass" |
|
540 "sublocale" |
|
541 "termination" |
|
542 "theorem" |
|
543 "typedef")) |
|
544 |
|
545 (defconst isar-keywords-qed |
|
546 '("\\." |
|
547 "\\.\\." |
|
548 "by" |
|
549 "done" |
|
550 "sorry")) |
|
551 |
|
552 (defconst isar-keywords-qed-block |
|
553 '("qed")) |
|
554 |
|
555 (defconst isar-keywords-qed-global |
|
556 '("oops")) |
|
557 |
|
558 (defconst isar-keywords-proof-heading |
|
559 '("sect" |
|
560 "subsect" |
|
561 "subsubsect")) |
|
562 |
|
563 (defconst isar-keywords-proof-goal |
|
564 '("have" |
|
565 "hence" |
|
566 "interpret")) |
|
567 |
|
568 (defconst isar-keywords-proof-block |
|
569 '("next" |
|
570 "proof")) |
|
571 |
|
572 (defconst isar-keywords-proof-open |
|
573 '("{")) |
|
574 |
|
575 (defconst isar-keywords-proof-close |
|
576 '("}")) |
|
577 |
|
578 (defconst isar-keywords-proof-chain |
|
579 '("finally" |
|
580 "from" |
|
581 "then" |
|
582 "ultimately" |
|
583 "with")) |
|
584 |
|
585 (defconst isar-keywords-proof-decl |
|
586 '("ML_prf" |
|
587 "also" |
|
588 "let" |
|
589 "moreover" |
|
590 "note" |
|
591 "txt" |
|
592 "txt_raw" |
|
593 "unfolding" |
|
594 "using")) |
|
595 |
|
596 (defconst isar-keywords-proof-asm |
|
597 '("assume" |
|
598 "case" |
|
599 "def" |
|
600 "fix" |
|
601 "presume")) |
|
602 |
|
603 (defconst isar-keywords-proof-asm-goal |
|
604 '("guess" |
|
605 "obtain" |
|
606 "show" |
|
607 "thus")) |
|
608 |
|
609 (defconst isar-keywords-proof-script |
|
610 '("apply" |
|
611 "apply_end" |
|
612 "back" |
|
613 "defer" |
|
614 "prefer")) |
|
615 |
|
616 (provide 'isar-keywords) |