author | wenzelm |
Sun, 28 Jul 2019 12:35:59 +0200 | |
changeset 70428 | 4537e82019d3 |
parent 70427 | 973bf3e42e54 |
child 70430 | 6ec97dc6670e |
permissions | -rw-r--r-- |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
1 |
(* Title: Pure/global_theory.ML |
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
2 |
Author: Makarius |
3987 | 3 |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
4 |
Global theory content: stored facts. |
3987 | 5 |
*) |
6 |
||
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
7 |
signature GLOBAL_THEORY = |
3987 | 8 |
sig |
27198 | 9 |
val facts_of: theory -> Facts.T |
56003 | 10 |
val check_fact: theory -> xstring * Position.T -> string |
26666 | 11 |
val intern_fact: theory -> xstring -> string |
26693 | 12 |
val defined_fact: theory -> string -> bool |
57887 | 13 |
val alias_fact: binding -> string -> theory -> theory |
27198 | 14 |
val hide_fact: bool -> string -> theory -> theory |
26344
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
15 |
val get_thms: theory -> xstring -> thm list |
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
16 |
val get_thm: theory -> xstring -> thm |
61054 | 17 |
val transfer_theories: theory -> thm -> thm |
56161 | 18 |
val all_thms_of: theory -> bool -> (string * thm) list |
21580 | 19 |
val map_facts: ('a -> 'b) -> ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
21567 | 20 |
val burrow_fact: ('a list -> 'b list) -> ('a list * 'c) list -> ('b list * 'c) list |
21580 | 21 |
val burrow_facts: ('a list -> 'b list) -> |
22 |
('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list |
|
23 |
val name_multi: string -> 'a list -> (string * 'a) list |
|
70427 | 24 |
type name_flags = {pre: bool, official: bool} |
25 |
val official1: name_flags |
|
26 |
val official2: name_flags |
|
27 |
val unofficial1: name_flags |
|
28 |
val unofficial2: name_flags |
|
29 |
val name_thm: name_flags -> string -> thm -> thm |
|
30 |
val name_thms: name_flags -> string -> thm list -> thm list |
|
68661 | 31 |
val check_thms_lazy: thm list lazy -> thm list lazy |
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67663
diff
changeset
|
32 |
val add_thms_lazy: string -> (binding * thm list lazy) -> theory -> theory |
29579 | 33 |
val store_thm: binding * thm -> theory -> thm * theory |
34 |
val store_thm_open: binding * thm -> theory -> thm * theory |
|
35 |
val add_thms: ((binding * thm) * attribute list) list -> theory -> thm list * theory |
|
36 |
val add_thm: (binding * thm) * attribute list -> theory -> thm * theory |
|
37 |
val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory |
|
57929
c5063c033a5a
tuned signature -- proper Local_Theory.add_thms_dynamic;
wenzelm
parents:
57887
diff
changeset
|
38 |
val add_thms_dynamic': Context.generic -> binding * (Context.generic -> thm list) -> |
c5063c033a5a
tuned signature -- proper Local_Theory.add_thms_dynamic;
wenzelm
parents:
57887
diff
changeset
|
39 |
theory -> string * theory |
29579 | 40 |
val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory |
67713 | 41 |
val note_thms: string -> Thm.binding * (thm list * attribute list) list -> theory -> |
42 |
(string * thm list) * theory |
|
43 |
val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list -> theory -> |
|
44 |
(string * thm list) list * theory |
|
29579 | 45 |
val add_defs: bool -> ((binding * term) * attribute list) list -> |
18377 | 46 |
theory -> thm list * theory |
29579 | 47 |
val add_defs_unchecked: bool -> ((binding * term) * attribute list) list -> |
48 |
theory -> thm list * theory |
|
3987 | 49 |
end; |
50 |
||
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
51 |
structure Global_Theory: GLOBAL_THEORY = |
3987 | 52 |
struct |
53 |
||
27198 | 54 |
(** theory data **) |
26282
305d5ca4fa9d
replaced obsolete FactIndex.T by Facts.T (cumulative version, assumes that facts are only added to unfinished theories);
wenzelm
parents:
26050
diff
changeset
|
55 |
|
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
39507
diff
changeset
|
56 |
structure Data = Theory_Data |
24713 | 57 |
( |
49010 | 58 |
type T = Facts.T; |
59 |
val empty = Facts.empty; |
|
60 |
val extend = I; |
|
61 |
val merge = Facts.merge; |
|
24713 | 62 |
); |
3987 | 63 |
|
49010 | 64 |
val facts_of = Data.get; |
26666 | 65 |
|
56003 | 66 |
fun check_fact thy = Facts.check (Context.Theory thy) (facts_of thy); |
26666 | 67 |
val intern_fact = Facts.intern o facts_of; |
26693 | 68 |
val defined_fact = Facts.defined o facts_of; |
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
69 |
|
57887 | 70 |
fun alias_fact binding name thy = |
71 |
Data.map (Facts.alias (Sign.naming_of thy) binding name) thy; |
|
72 |
||
49010 | 73 |
fun hide_fact fully name = Data.map (Facts.hide fully name); |
6367 | 74 |
|
3987 | 75 |
|
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56003
diff
changeset
|
76 |
(* retrieve theorems *) |
27198 | 77 |
|
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56003
diff
changeset
|
78 |
fun get_thms thy xname = |
57942
e5bec882fdd0
more informative Token.Fact: retain name of dynamic fact (without selection);
wenzelm
parents:
57929
diff
changeset
|
79 |
#thms (Facts.retrieve (Context.Theory thy) (facts_of thy) (xname, Position.none)); |
26344
04dacc6809b6
simplified get_thm(s): back to plain name argument;
wenzelm
parents:
26336
diff
changeset
|
80 |
|
56140
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56003
diff
changeset
|
81 |
fun get_thm thy xname = |
ed92ce2ac88e
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
wenzelm
parents:
56003
diff
changeset
|
82 |
Facts.the_single (xname, Position.none) (get_thms thy xname); |
4783 | 83 |
|
61054 | 84 |
fun transfer_theories thy = |
85 |
let |
|
86 |
val theories = |
|
87 |
fold (fn thy' => Symtab.update (Context.theory_name thy', thy')) |
|
88 |
(Theory.nodes_of thy) Symtab.empty; |
|
89 |
fun transfer th = |
|
65458 | 90 |
Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name th))) th; |
61054 | 91 |
in transfer end; |
92 |
||
56161 | 93 |
fun all_thms_of thy verbose = |
94 |
let |
|
61054 | 95 |
val transfer = transfer_theories thy; |
56161 | 96 |
val facts = facts_of thy; |
97 |
fun add (name, ths) = |
|
98 |
if not verbose andalso Facts.is_concealed facts name then I |
|
61054 | 99 |
else append (map (`(Thm.get_name_hint) o transfer) ths); |
56161 | 100 |
in Facts.fold_static add facts [] end; |
16336 | 101 |
|
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
102 |
|
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
103 |
|
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
104 |
(** store theorems **) |
3987 | 105 |
|
21580 | 106 |
(* fact specifications *) |
107 |
||
108 |
fun map_facts f = map (apsnd (map (apfst (map f)))); |
|
109 |
fun burrow_fact f = split_list #>> burrow f #> op ~~; |
|
110 |
fun burrow_facts f = split_list ##> burrow (burrow_fact f) #> op ~~; |
|
111 |
||
112 |
||
4853 | 113 |
(* naming *) |
114 |
||
70427 | 115 |
type name_flags = {pre: bool, official: bool}; |
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
116 |
|
70427 | 117 |
val official1 : name_flags = {pre = true, official = true}; |
118 |
val official2 : name_flags = {pre = false, official = true}; |
|
119 |
val unofficial1 : name_flags = {pre = true, official = false}; |
|
120 |
val unofficial2 : name_flags = {pre = false, official = false}; |
|
121 |
||
122 |
fun name_thm {pre, official} name thm = thm |
|
70426 | 123 |
|> (official andalso not (pre andalso Thm.derivation_name thm <> "")) ? |
124 |
Thm.name_derivation name |
|
125 |
|> (name <> "" andalso not (pre andalso Thm.has_name_hint thm)) ? |
|
126 |
Thm.put_name_hint name; |
|
12872
0855c3ab2047
Theorems are only "pre-named" if the do not already have names.
berghofe
parents:
12711
diff
changeset
|
127 |
|
70427 | 128 |
|
129 |
fun name_multi name [x] = [(name, x)] |
|
130 |
| name_multi "" xs = map (pair "") xs |
|
131 |
| name_multi name xs = map_index (fn (i, x) => (name ^ "_" ^ string_of_int (i + 1), x)) xs; |
|
132 |
||
133 |
fun name_thms name_flags name thms = |
|
134 |
map (uncurry (name_thm name_flags)) (name_multi name thms); |
|
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
135 |
|
4853 | 136 |
|
70424 | 137 |
(* apply theorems and attributes *) |
4853 | 138 |
|
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67663
diff
changeset
|
139 |
fun register_proofs thms thy = (thms, Thm.register_proofs (Lazy.value thms) thy); |
49010 | 140 |
|
68244
e0cd57aeb60c
more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
wenzelm
parents:
67779
diff
changeset
|
141 |
fun add_facts (b, fact) thy = |
e0cd57aeb60c
more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
wenzelm
parents:
67779
diff
changeset
|
142 |
let |
e0cd57aeb60c
more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
wenzelm
parents:
67779
diff
changeset
|
143 |
val full_name = Sign.full_name thy b; |
e0cd57aeb60c
more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
wenzelm
parents:
67779
diff
changeset
|
144 |
val pos = Binding.pos_of b; |
68540 | 145 |
fun check fact = |
146 |
fact |> map_index (fn (i, thm) => |
|
147 |
let |
|
148 |
fun err msg = |
|
149 |
error ("Malformed global fact " ^ |
|
150 |
quote (full_name ^ |
|
151 |
(if length fact = 1 then "" else "(" ^ string_of_int (i + 1) ^ ")")) ^ |
|
152 |
Position.here pos ^ "\n" ^ msg); |
|
153 |
val prop = Thm.plain_prop_of thm |
|
154 |
handle THM _ => |
|
155 |
thm |
|
156 |
|> Thm.check_hyps (Context.Theory thy) |
|
157 |
|> Thm.full_prop_of; |
|
158 |
in |
|
159 |
ignore (Logic.unvarify_global (Term_Subst.zero_var_indexes prop)) |
|
160 |
handle TYPE (msg, _, _) => err msg |
|
161 |
| TERM (msg, _) => err msg |
|
162 |
| ERROR msg => err msg |
|
163 |
end); |
|
164 |
val arg = (b, Lazy.map_finished (tap check) fact); |
|
68244
e0cd57aeb60c
more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
wenzelm
parents:
67779
diff
changeset
|
165 |
in |
e0cd57aeb60c
more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
wenzelm
parents:
67779
diff
changeset
|
166 |
thy |> Data.map (Facts.add_static (Context.Theory thy) {strict = true, index = false} arg #> #2) |
e0cd57aeb60c
more checks for global facts: disallow undeclared frees (as in Export_Theory.export_fact);
wenzelm
parents:
67779
diff
changeset
|
167 |
end; |
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67663
diff
changeset
|
168 |
|
68661 | 169 |
fun check_thms_lazy (thms: thm list lazy) = |
68701
be936cf061ab
more robust: do not defer potentially slow/big lazy facts to the very end;
wenzelm
parents:
68699
diff
changeset
|
170 |
if Proofterm.proofs_enabled () orelse Options.default_bool "strict_facts" |
be936cf061ab
more robust: do not defer potentially slow/big lazy facts to the very end;
wenzelm
parents:
68699
diff
changeset
|
171 |
then Lazy.force_value thms else thms; |
68661 | 172 |
|
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67663
diff
changeset
|
173 |
fun add_thms_lazy kind (b, thms) thy = |
68661 | 174 |
if Binding.is_empty b then Thm.register_proofs (check_thms_lazy thms) thy |
30211 | 175 |
else |
176 |
let |
|
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46775
diff
changeset
|
177 |
val name = Sign.full_name thy b; |
68661 | 178 |
val thms' = |
179 |
check_thms_lazy thms |
|
70427 | 180 |
|> Lazy.map_finished (name_thms official1 name #> map (Thm.kind_rule kind)); |
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67663
diff
changeset
|
181 |
in thy |> Thm.register_proofs thms' |> add_facts (b, thms') end; |
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67663
diff
changeset
|
182 |
|
70424 | 183 |
val app_facts = |
184 |
apfst flat oo fold_map (fn (thms, atts) => fold_map (Thm.theory_attributes atts) thms); |
|
185 |
||
186 |
fun apply_facts pre_name post_name (b, facts) thy = |
|
187 |
if Binding.is_empty b then app_facts facts thy |-> register_proofs |
|
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67663
diff
changeset
|
188 |
else |
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67663
diff
changeset
|
189 |
let |
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67663
diff
changeset
|
190 |
val name = Sign.full_name thy b; |
70424 | 191 |
val (thms', thy') = thy |
192 |
|> app_facts (map (apfst (pre_name name)) facts) |
|
193 |
|>> post_name name |-> register_proofs; |
|
67671
857da80611ab
support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes;
wenzelm
parents:
67663
diff
changeset
|
194 |
val thy'' = thy' |> add_facts (b, Lazy.value thms'); |
67663 | 195 |
in (map (Thm.transfer thy'') thms', thy'') end; |
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
196 |
|
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
197 |
|
67715 | 198 |
(* store_thm *) |
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
199 |
|
67715 | 200 |
fun store_thm (b, th) = |
70427 | 201 |
apply_facts (name_thms official1) (name_thms official2) (b, [([th], [])]) #>> the_single; |
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
202 |
|
29579 | 203 |
fun store_thm_open (b, th) = |
70427 | 204 |
apply_facts (name_thms unofficial1) (name_thms unofficial2) (b, [([th], [])]) #>> the_single; |
3987 | 205 |
|
16023
66561f6814bd
added string_of_thmref, selections, fact_index_of, valid_thms;
wenzelm
parents:
15975
diff
changeset
|
206 |
|
6091 | 207 |
(* add_thms(s) *) |
4853 | 208 |
|
70428 | 209 |
val add_thmss = |
210 |
fold_map (fn ((b, thms), atts) => |
|
211 |
apply_facts (name_thms official1) (name_thms official2) (b, [(thms, atts)])); |
|
5907 | 212 |
|
70428 | 213 |
fun add_thms args = |
214 |
add_thmss (map (apfst (apsnd single)) args) #>> map the_single; |
|
12235
5fa04fc9b254
Further restructuring of theorem naming functions.
berghofe
parents:
12138
diff
changeset
|
215 |
|
27683 | 216 |
val add_thm = yield_singleton add_thms; |
5907 | 217 |
|
218 |
||
57929
c5063c033a5a
tuned signature -- proper Local_Theory.add_thms_dynamic;
wenzelm
parents:
57887
diff
changeset
|
219 |
(* dynamic theorems *) |
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
220 |
|
57929
c5063c033a5a
tuned signature -- proper Local_Theory.add_thms_dynamic;
wenzelm
parents:
57887
diff
changeset
|
221 |
fun add_thms_dynamic' context arg thy = |
c5063c033a5a
tuned signature -- proper Local_Theory.add_thms_dynamic;
wenzelm
parents:
57887
diff
changeset
|
222 |
let val (name, facts') = Facts.add_dynamic context arg (Data.get thy) |
c5063c033a5a
tuned signature -- proper Local_Theory.add_thms_dynamic;
wenzelm
parents:
57887
diff
changeset
|
223 |
in (name, Data.put facts' thy) end; |
c5063c033a5a
tuned signature -- proper Local_Theory.add_thms_dynamic;
wenzelm
parents:
57887
diff
changeset
|
224 |
|
c5063c033a5a
tuned signature -- proper Local_Theory.add_thms_dynamic;
wenzelm
parents:
57887
diff
changeset
|
225 |
fun add_thms_dynamic arg thy = |
c5063c033a5a
tuned signature -- proper Local_Theory.add_thms_dynamic;
wenzelm
parents:
57887
diff
changeset
|
226 |
add_thms_dynamic' (Context.Theory thy) arg thy |> snd; |
26488
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
227 |
|
b497e3187ec7
eliminated destructive/critical theorem database;
wenzelm
parents:
26471
diff
changeset
|
228 |
|
27728 | 229 |
(* note_thmss *) |
5907 | 230 |
|
67713 | 231 |
fun note_thms kind ((b, more_atts), facts) thy = |
12711 | 232 |
let |
28965 | 233 |
val name = Sign.full_name thy b; |
70424 | 234 |
val facts' = facts |> map (apsnd (fn atts => surround (Thm.kind kind) (atts @ more_atts))); |
70427 | 235 |
val (thms', thy') = thy |> apply_facts (name_thms official1) (name_thms official2) (b, facts'); |
70424 | 236 |
in ((name, thms'), thy') end; |
67713 | 237 |
|
238 |
val note_thmss = fold_map o note_thms; |
|
12711 | 239 |
|
5280 | 240 |
|
62170 | 241 |
(* old-style defs *) |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
242 |
|
4853 | 243 |
local |
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
244 |
|
62169 | 245 |
fun add unchecked overloaded = fold_map (fn ((b, prop), atts) => fn thy => |
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
246 |
let |
62170 | 247 |
val context = Defs.global_context thy; |
61262
7bd1eb4b056e
tuned signature: eliminated pointless type Context.pretty;
wenzelm
parents:
61261
diff
changeset
|
248 |
val ((_, def), thy') = Thm.add_def context unchecked overloaded (b, prop) thy; |
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
249 |
val thm = def |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
250 |
|> Thm.forall_intr_frees |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
251 |
|> Thm.forall_elim_vars 0 |
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
252 |
|> Thm.varifyT_global; |
70428 | 253 |
in |
254 |
thy' |
|
255 |
|> apply_facts (K I) (name_thms official2) (b, [([thm], atts)]) |
|
256 |
|>> the_single |
|
257 |
end); |
|
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
258 |
|
4853 | 259 |
in |
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
260 |
|
62169 | 261 |
val add_defs = add false; |
262 |
val add_defs_unchecked = add true; |
|
35985
0bbf0d2348f9
moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
wenzelm
parents:
35856
diff
changeset
|
263 |
|
4853 | 264 |
end; |
4022
0770a19c48d3
added ignored_consts, thms_containing, add_store_axioms(_i),
wenzelm
parents:
4013
diff
changeset
|
265 |
|
3987 | 266 |
end; |