equal
deleted
inserted
replaced
228 (cat_lines ["Declaration of equivariance lemmas - they will automtically be", |
228 (cat_lines ["Declaration of equivariance lemmas - they will automtically be", |
229 "brought into the form p o c == c"]) #> |
229 "brought into the form p o c == c"]) #> |
230 Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) |
230 Attrib.setup @{binding "eqvt_raw"} (Attrib.add_del eqvt_raw_add eqvt_raw_del) |
231 (cat_lines ["Declaration of equivariance lemmas - no", |
231 (cat_lines ["Declaration of equivariance lemmas - no", |
232 "transformation is performed"]) #> |
232 "transformation is performed"]) #> |
233 PureThy.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> |
233 Global_Theory.add_thms_dynamic (@{binding "eqvts"}, eqvts) #> |
234 PureThy.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw); |
234 Global_Theory.add_thms_dynamic (@{binding "eqvts_raw"}, eqvts_raw); |
235 |
235 |
236 |
236 |
237 end; |
237 end; |