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