1 (* Title: nominal_thmdecls.ML |
1 (* Title: nominal_thmdecls.ML |
2 Author: Christian Urban |
2 Author: Christian Urban |
3 |
3 Author: Tjark Weber |
4 Infrastructure for the lemma collection "eqvts". |
4 |
|
5 Infrastructure for the lemma collections "eqvts", "eqvts_raw". |
5 |
6 |
6 Provides the attributes [eqvt] and [eqvt_raw], and the theorem |
7 Provides the attributes [eqvt] and [eqvt_raw], and the theorem |
7 lists eqvts and eqvts_raw. The first attribute will store the |
8 lists "eqvts" and "eqvts_raw". |
8 theorem in the eqvts list and also in the eqvts_raw list. For |
9 |
9 the latter the theorem is expected to be of the form |
10 The [eqvt] attribute expects a theorem of the form |
10 |
11 |
11 p o (c x1 x2 ...) = c (p o x1) (p o x2) ... (1) |
12 ?p \<bullet> (c ?x1 ?x2 ...) = c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ... (1) |
12 |
13 |
13 or |
14 or, if c is a relation with arity >= 1, of the form |
14 |
15 |
15 c x1 x2 ... ==> c (p o x1) (p o x2) ... (2) |
16 c ?x1 ?x2 ... ==> c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ... (2) |
16 |
17 |
17 and it is stored in the form |
18 [eqvt] will store this theorem in the form (1) or, if c |
18 |
19 is a relation with arity >= 1, in the form |
19 p o c == c |
20 |
20 |
21 c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ... = c ?x1 ?x2 ... (3) |
21 The [eqvt_raw] attribute just adds the theorem to eqvts_raw. |
22 |
22 |
23 in "eqvts". (The orientation of (3) was chosen because |
23 TODO: In case of the form in (2) one should also |
24 Isabelle's simplifier uses equations from left to right.) |
24 add the equational form to eqvts |
25 [eqvt] will also derive and store the theorem |
|
26 |
|
27 ?p \<bullet> c == c (4) |
|
28 |
|
29 in "eqvts_raw". |
|
30 |
|
31 (1)-(4) are all logically equivalent. We consider (1) and (2) |
|
32 to be more end-user friendly, i.e., slightly more natural to |
|
33 understand and prove, while (3) and (4) make the rewriting |
|
34 system for equivariance more predictable and less prone to |
|
35 looping in Isabelle. |
|
36 |
|
37 The [eqvt_raw] attribute expects a theorem of the form (4), |
|
38 and merely stores it in "eqvts_raw". |
|
39 |
|
40 [eqvt_raw] is provided because certain equivariance theorems |
|
41 would lead to looping when used for simplification in the form |
|
42 (1): notably, equivariance of permute (infix \<bullet>), i.e., |
|
43 ?p \<bullet> (?q \<bullet> ?x) = (?p \<bullet> ?q) \<bullet> (?p \<bullet> ?x). |
|
44 |
|
45 To support binders such as All/Ex/Ball/Bex etc., which are |
|
46 typically applied to abstractions, argument terms ?xi (as well |
|
47 as permuted arguments ?p \<bullet> ?xi) in (1)-(3) need not be eta- |
|
48 contracted, i.e., they may be of the form "%z. ?xi z" or |
|
49 "%z. (?p \<bullet> ?x) z", respectively. |
|
50 |
|
51 For convenience, argument terms ?xi (as well as permuted |
|
52 arguments ?p \<bullet> ?xi) in (1)-(3) may actually be tuples, e.g., |
|
53 "(?xi, ?xj)" or "(?p \<bullet> ?xi, ?p \<bullet> ?xj)", respectively. |
|
54 |
|
55 In (1)-(4), "c" is either a (global) constant or a locally |
|
56 fixed parameter, e.g., of a locale or type class. |
25 *) |
57 *) |
26 |
58 |
27 signature NOMINAL_THMDECLS = |
59 signature NOMINAL_THMDECLS = |
28 sig |
60 sig |
29 val eqvt_add: attribute |
61 val eqvt_add: attribute |
44 ( type T = thm Item_Net.T; |
76 ( type T = thm Item_Net.T; |
45 val empty = Thm.full_rules; |
77 val empty = Thm.full_rules; |
46 val extend = I; |
78 val extend = I; |
47 val merge = Item_Net.merge); |
79 val merge = Item_Net.merge); |
48 |
80 |
|
81 (* EqvtRawData is implemented with a Termtab (rather than an |
|
82 Item_Net) so that we can efficiently decide whether a given |
|
83 constant has a corresponding equivariance theorem stored, cf. |
|
84 the function is_eqvt. *) |
49 structure EqvtRawData = Generic_Data |
85 structure EqvtRawData = Generic_Data |
50 ( type T = thm Termtab.table; |
86 ( type T = thm Termtab.table; |
51 val empty = Termtab.empty; |
87 val empty = Termtab.empty; |
52 val extend = I; |
88 val extend = I; |
53 val merge = Termtab.merge (K true)); |
89 val merge = Termtab.merge (K true)); |
54 |
90 |
55 val eqvts = Item_Net.content o EqvtData.get; |
91 val eqvts = Item_Net.content o EqvtData.get |
56 val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get; |
92 val eqvts_raw = map snd o Termtab.dest o EqvtRawData.get |
57 |
93 |
58 val get_eqvts_thms = eqvts o Context.Proof; |
94 val get_eqvts_thms = eqvts o Context.Proof |
59 val get_eqvts_raw_thms = eqvts_raw o Context.Proof; |
95 val get_eqvts_raw_thms = eqvts_raw o Context.Proof |
60 |
96 |
61 fun checked_update key net = |
97 |
62 (if Item_Net.member net key then |
98 (** raw equivariance lemmas **) |
63 warning "Theorem already declared as equivariant." |
99 |
64 else (); |
100 (* Returns true iff an equivariance lemma exists in "eqvts_raw" |
65 Item_Net.update key net) |
101 for a given term. *) |
66 |
102 val is_eqvt = |
67 val add_thm = EqvtData.map o checked_update; |
103 Termtab.defined o EqvtRawData.get o Context.Proof |
68 val del_thm = EqvtData.map o Item_Net.remove; |
104 |
69 |
105 (* Returns c if thm is of the form (4), raises an error |
70 fun add_raw_thm thm = |
106 otherwise. *) |
71 case prop_of thm of |
107 fun key_of_raw_thm context thm = |
72 Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.update (c, thm)) |
108 let |
73 | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) |
109 fun error_msg () = |
74 |
110 error |
75 fun del_raw_thm thm = |
111 ("Theorem must be of the form \"?p \<bullet> c \<equiv> c\", with c a constant or fixed parameter:\n" ^ |
76 case prop_of thm of |
112 Syntax.string_of_term (Context.proof_of context) (prop_of thm)) |
77 Const ("==", _) $ _ $ (c as Const _) => EqvtRawData.map (Termtab.delete c) |
113 in |
78 | _ => raise THM ("Theorem must be a meta-equality where the right-hand side is a constant.", 0, [thm]) |
114 case prop_of thm of |
79 |
115 Const ("==", _) $ (Const (@{const_name "permute"}, _) $ p $ c) $ c' => |
80 fun is_eqvt ctxt trm = |
116 if is_Var p andalso is_fixed (Context.proof_of context) c andalso c aconv c' then |
81 case trm of |
117 c |
82 (c as Const _) => Termtab.defined (EqvtRawData.get (Context.Proof ctxt)) c |
118 else |
83 | _ => false (* raise TERM ("Term must be a constant.", [trm]) *) |
119 error_msg () |
84 |
120 | _ => error_msg () |
85 |
121 end |
86 |
122 |
87 (** transformation of eqvt lemmas **) |
123 fun add_raw_thm thm context = |
88 |
124 let |
89 fun get_perms trm = |
125 val c = key_of_raw_thm context thm |
90 case trm of |
126 in |
91 Const (@{const_name permute}, _) $ _ $ (Bound _) => |
127 if Termtab.defined (EqvtRawData.get context) c then |
92 raise TERM ("get_perms called on bound", [trm]) |
128 warning ("Replacing existing raw equivariance theorem for \"" ^ |
93 | Const (@{const_name permute}, _) $ p $ _ => [p] |
129 Syntax.string_of_term (Context.proof_of context) c ^ "\".") |
94 | t $ u => get_perms t @ get_perms u |
130 else (); |
95 | Abs (_, _, t) => get_perms t |
131 EqvtRawData.map (Termtab.update (c, thm)) context |
96 | _ => [] |
132 end |
97 |
133 |
98 fun add_perm p trm = |
134 fun del_raw_thm thm context = |
99 let |
135 let |
100 fun aux trm = |
136 val c = key_of_raw_thm context thm |
101 case trm of |
137 in |
102 Bound _ => trm |
138 if Termtab.defined (EqvtRawData.get context) c then |
103 | Const _ => trm |
139 EqvtRawData.map (Termtab.delete c) context |
104 | t $ u => aux t $ aux u |
140 else ( |
105 | Abs (x, ty, t) => Abs (x, ty, aux t) |
141 warning ("Cannot delete non-existing raw equivariance theorem for \"" ^ |
106 | _ => mk_perm p trm |
142 Syntax.string_of_term (Context.proof_of context) c ^ "\"."); |
107 in |
143 context |
108 strip_comb trm |
144 ) |
109 ||> map aux |
145 end |
110 |> list_comb |
146 |
111 end |
147 |
112 |
148 (** adding/deleting lemmas to/from "eqvts" **) |
113 |
149 |
114 (* tests whether there is a disagreement between the permutations, |
150 fun add_thm thm context = |
115 and that there is at least one permutation *) |
151 ( |
116 fun is_bad_list [] = true |
152 if Item_Net.member (EqvtData.get context) thm then |
117 | is_bad_list [_] = false |
153 warning ("Theorem already declared as equivariant:\n" ^ |
118 | is_bad_list (p::q::ps) = if p = q then is_bad_list (q::ps) else true |
154 Syntax.string_of_term (Context.proof_of context) (prop_of thm)) |
119 |
155 else (); |
120 |
156 EqvtData.map (Item_Net.update thm) context |
121 (* transforms equations into the "p o c == c"-form |
157 ) |
122 from p o (c x1 ...xn) = c (p o x1) ... (p o xn) *) |
158 |
123 |
159 fun del_thm thm context = |
124 fun eqvt_transform_eq_tac thm = |
160 ( |
125 let |
161 if Item_Net.member (EqvtData.get context) thm then |
126 val ss_thms = @{thms permute_minus_cancel permute_prod.simps split_paired_all} |
162 EqvtData.map (Item_Net.remove thm) context |
|
163 else ( |
|
164 warning ("Cannot delete non-existing equivariance theorem:\n" ^ |
|
165 Syntax.string_of_term (Context.proof_of context) (prop_of thm)); |
|
166 context |
|
167 ) |
|
168 ) |
|
169 |
|
170 |
|
171 (** transformation of equivariance lemmas **) |
|
172 |
|
173 (* Transforms a theorem of the form (1) into the form (4). *) |
|
174 local |
|
175 |
|
176 fun tac thm = |
|
177 let |
|
178 val ss_thms = @{thms "permute_minus_cancel" "permute_prod.simps" "split_paired_all"} |
|
179 in |
|
180 REPEAT o FIRST' |
|
181 [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms), |
|
182 rtac (thm RS @{thm "trans"}), |
|
183 rtac @{thm "trans"[OF "permute_fun_def"]} THEN' rtac @{thm "ext"}] |
|
184 end |
|
185 |
127 in |
186 in |
128 REPEAT o FIRST' |
187 |
129 [CHANGED o simp_tac (HOL_basic_ss addsimps ss_thms), |
188 fun thm_4_of_1 ctxt thm = |
130 rtac (thm RS @{thm trans}), |
189 let |
131 rtac @{thm trans[OF permute_fun_def]} THEN' rtac @{thm ext}] |
190 val (p, c) = thm |> prop_of |> HOLogic.dest_Trueprop |
132 end |
191 |> HOLogic.dest_eq |> fst |> dest_perm ||> fst o (fixed_nonfixed_args ctxt) |
133 |
192 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
134 fun eqvt_transform_eq ctxt thm = |
193 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
135 let |
194 in |
136 val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm)) |
195 Goal.prove ctxt [] [] goal' (fn _ => tac thm 1) |
137 handle TERM _ => error "Equivariance lemma must be an equality." |
196 |> singleton (Proof_Context.export ctxt' ctxt) |
138 val (p, t) = dest_perm lhs |
197 |> (fn th => th RS @{thm "eq_reflection"}) |
139 handle TERM _ => error "Equivariance lemma is not of the form p \<bullet> c... = c..." |
198 |> zero_var_indexes |
140 |
199 end |
141 val ps = get_perms rhs handle TERM _ => [] |
200 handle TERM _ => |
142 val (c, c') = (head_of t, head_of rhs) |
201 raise THM ("thm_4_of_1", 0, [thm]) |
143 val msg = "Equivariance lemma is not of the right form " |
202 |
144 in |
203 end (* local *) |
145 if c <> c' |
204 |
146 then error (msg ^ "(constants do not agree).") |
205 (* Transforms a theorem of the form (2) into the form (1). *) |
147 else if is_bad_list (p :: ps) |
206 local |
148 then error (msg ^ "(permutations do not agree).") |
207 |
149 else if not (rhs aconv (add_perm p t)) |
208 fun tac thm thm' = |
150 then error (msg ^ "(arguments do not agree).") |
209 let |
151 else if is_Const t |
210 val ss_thms = @{thms "permute_minus_cancel"(2)} |
152 then safe_mk_equiv thm |
211 in |
153 else |
212 EVERY' [rtac @{thm "iffI"}, dtac @{thm "permute_boolE"}, rtac thm, atac, |
154 let |
213 rtac @{thm "permute_boolI"}, dtac thm', full_simp_tac (HOL_basic_ss addsimps ss_thms)] |
155 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p c, c)) |
214 end |
156 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
215 |
|
216 in |
|
217 |
|
218 fun thm_1_of_2 ctxt thm = |
|
219 let |
|
220 val (prem, concl) = thm |> prop_of |> Logic.dest_implies |> pairself HOLogic.dest_Trueprop |
|
221 (* since argument terms "?p \<bullet> ?x1" may actually be eta-expanded |
|
222 or tuples, we need the following function to find ?p *) |
|
223 fun find_perm (Const (@{const_name "permute"}, _) $ (p as Var _) $ _) = p |
|
224 | find_perm (Const (@{const_name "Pair"}, _) $ x $ _) = find_perm x |
|
225 | find_perm (Abs (_, _, body)) = find_perm body |
|
226 | find_perm _ = raise THM ("thm_3_of_2", 0, [thm]) |
|
227 val p = concl |> dest_comb |> snd |> find_perm |
|
228 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_perm p prem, concl)) |
|
229 val ([goal', p'], ctxt') = Variable.import_terms false [goal, p] ctxt |
|
230 val certify = cterm_of (theory_of_thm thm) |
|
231 val thm' = Drule.cterm_instantiate [(certify p, certify (mk_minus p'))] thm |
|
232 in |
|
233 Goal.prove ctxt' [] [] goal' (fn _ => tac thm thm' 1) |
|
234 |> singleton (Proof_Context.export ctxt' ctxt) |
|
235 end |
|
236 handle TERM _ => |
|
237 raise THM ("thm_1_of_2", 0, [thm]) |
|
238 |
|
239 end (* local *) |
|
240 |
|
241 (* Transforms a theorem of the form (1) into the form (3). *) |
|
242 fun thm_3_of_1 _ thm = |
|
243 (thm RS (@{thm "permute_bool_def"} RS @{thm "sym"} RS @{thm "trans"}) RS @{thm "sym"}) |
|
244 |> zero_var_indexes |
|
245 |
|
246 local |
|
247 val msg = cat_lines |
|
248 ["Equivariance theorem must be of the form", |
|
249 " ?p \<bullet> (c ?x1 ?x2 ...) = c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ...", |
|
250 "or, if c is a relation with arity >= 1, of the form", |
|
251 " c ?x1 ?x2 ... ==> c (?p \<bullet> ?x1) (?p \<bullet> ?x2) ..."] |
|
252 in |
|
253 |
|
254 (* Transforms a theorem of the form (1) or (2) into the form (4). *) |
|
255 fun eqvt_transform ctxt thm = |
|
256 (case prop_of thm of @{const "Trueprop"} $ _ => |
|
257 thm_4_of_1 ctxt thm |
|
258 | @{const "==>"} $ _ $ _ => |
|
259 thm_4_of_1 ctxt (thm_1_of_2 ctxt thm) |
|
260 | _ => |
|
261 error msg) |
|
262 handle THM _ => |
|
263 error msg |
|
264 |
|
265 (* Transforms a theorem of the form (1) into theorems of the |
|
266 form (1) (or, if c is a relation with arity >= 1, of the form |
|
267 (3)) and (4); transforms a theorem of the form (2) into |
|
268 theorems of the form (3) and (4). *) |
|
269 fun eqvt_and_raw_transform ctxt thm = |
|
270 (case prop_of thm of @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ _ $ c_args) => |
|
271 let |
|
272 val th' = |
|
273 if fastype_of c_args = @{typ "bool"} |
|
274 andalso (not o null) (snd (fixed_nonfixed_args ctxt c_args)) then |
|
275 thm_3_of_1 ctxt thm |
|
276 else |
|
277 thm |
|
278 in |
|
279 (th', thm_4_of_1 ctxt thm) |
|
280 end |
|
281 | @{const "==>"} $ _ $ _ => |
|
282 let |
|
283 val th1 = thm_1_of_2 ctxt thm |
|
284 in |
|
285 (thm_3_of_1 ctxt th1, thm_4_of_1 ctxt th1) |
|
286 end |
|
287 | _ => |
|
288 error msg) |
|
289 handle THM _ => |
|
290 error msg |
|
291 |
|
292 end (* local *) |
|
293 |
|
294 |
|
295 (** attributes **) |
|
296 |
|
297 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm |
|
298 val eqvt_raw_del = Thm.declaration_attribute del_raw_thm |
|
299 |
|
300 fun eqvt_add_or_del eqvt_fn raw_fn = |
|
301 Thm.declaration_attribute |
|
302 (fn thm => fn context => |
|
303 let |
|
304 val (eqvt, raw) = eqvt_and_raw_transform (Context.proof_of context) thm |
157 in |
305 in |
158 Goal.prove ctxt [] [] goal' (fn _ => eqvt_transform_eq_tac thm 1) |
306 context |> eqvt_fn eqvt |> raw_fn raw |
159 |> singleton (Proof_Context.export ctxt' ctxt) |
307 end) |
160 |> safe_mk_equiv |
308 |
161 |> zero_var_indexes |
309 val eqvt_add = eqvt_add_or_del add_thm add_raw_thm |
162 end |
310 val eqvt_del = eqvt_add_or_del del_thm del_raw_thm |
163 end |
|
164 |
|
165 (* transforms equations into the "p o c == c"-form |
|
166 from R x1 ...xn ==> R (p o x1) ... (p o xn) *) |
|
167 |
|
168 fun eqvt_transform_imp_tac ctxt p p' thm = |
|
169 let |
|
170 val thy = Proof_Context.theory_of ctxt |
|
171 val cp = Thm.cterm_of thy p |
|
172 val cp' = Thm.cterm_of thy (mk_minus p') |
|
173 val thm' = Drule.cterm_instantiate [(cp, cp')] thm |
|
174 val simp = HOL_basic_ss addsimps @{thms permute_minus_cancel(2)} |
|
175 in |
|
176 EVERY' [rtac @{thm iffI}, dtac @{thm permute_boolE}, rtac thm, atac, |
|
177 rtac @{thm permute_boolI}, dtac thm', full_simp_tac simp] |
|
178 end |
|
179 |
|
180 fun eqvt_transform_imp ctxt thm = |
|
181 let |
|
182 val (prem, concl) = pairself HOLogic.dest_Trueprop (Logic.dest_implies (prop_of thm)) |
|
183 val (c, c') = (head_of prem, head_of concl) |
|
184 val ps = get_perms concl handle TERM _ => [] |
|
185 val p = try hd ps |
|
186 val msg = "Equivariance lemma is not of the right form " |
|
187 in |
|
188 if c <> c' |
|
189 then error (msg ^ "(constants do not agree).") |
|
190 else if is_bad_list ps |
|
191 then error (msg ^ "(permutations do not agree).") |
|
192 else if not (concl aconv (add_perm (the p) prem)) |
|
193 then error (msg ^ "(arguments do not agree).") |
|
194 else |
|
195 let |
|
196 val prem' = mk_perm (the p) prem |
|
197 val goal = HOLogic.mk_Trueprop (HOLogic.mk_eq (prem', concl)) |
|
198 val ([goal', p'], ctxt') = Variable.import_terms false [goal, the p] ctxt |
|
199 in |
|
200 Goal.prove ctxt' [] [] goal' |
|
201 (fn _ => eqvt_transform_imp_tac ctxt' (the p) p' thm 1) |
|
202 |> singleton (Proof_Context.export ctxt' ctxt) |
|
203 end |
|
204 end |
|
205 |
|
206 fun eqvt_transform ctxt thm = |
|
207 case (prop_of thm) of |
|
208 @{const "Trueprop"} $ (Const (@{const_name "HOL.eq"}, _) $ |
|
209 (Const (@{const_name "permute"}, _) $ _ $ _) $ _) => |
|
210 eqvt_transform_eq ctxt thm |
|
211 | @{const "==>"} $ (@{const "Trueprop"} $ _) $ (@{const "Trueprop"} $ _) => |
|
212 eqvt_transform_imp ctxt thm |> eqvt_transform_eq ctxt |
|
213 | _ => raise error "Only _ = _ and _ ==> _ cases are implemented." |
|
214 |
|
215 |
|
216 (** attributes **) |
|
217 |
|
218 val eqvt_add = Thm.declaration_attribute |
|
219 (fn thm => fn context => |
|
220 let |
|
221 val thm' = eqvt_transform (Context.proof_of context) thm |
|
222 in |
|
223 context |> add_thm thm |> add_raw_thm thm' |
|
224 end) |
|
225 |
|
226 val eqvt_del = Thm.declaration_attribute |
|
227 (fn thm => fn context => |
|
228 let |
|
229 val thm' = eqvt_transform (Context.proof_of context) thm |
|
230 in |
|
231 context |> del_thm thm |> del_raw_thm thm' |
|
232 end) |
|
233 |
|
234 val eqvt_raw_add = Thm.declaration_attribute add_raw_thm; |
|
235 val eqvt_raw_del = Thm.declaration_attribute del_raw_thm; |
|
236 |
311 |
237 |
312 |
238 (** setup function **) |
313 (** setup function **) |
239 |
314 |
240 val setup = |
315 val setup = |
241 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
316 Attrib.setup @{binding "eqvt"} (Attrib.add_del eqvt_add eqvt_del) |
242 (cat_lines ["Declaration of equivariance lemmas - they will automtically be", |
317 "Declaration of equivariance lemmas - they will automatically be brought into the form ?p \<bullet> c \<equiv> c" #> |
243 "brought into the form p o c == c"]) #> |
318 Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) |
244 Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) |
319 "Declaration of raw equivariance lemmas - no transformation is performed" #> |
245 (cat_lines ["Declaration of equivariance lemmas - no", |
|
246 "transformation is performed"]) #> |
|
247 Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> |
320 Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> |
248 Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw); |
321 Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw) |
249 |
|
250 |
322 |
251 end; |
323 end; |