equal
deleted
inserted
replaced
111 (cat_lines ["declaration of equivariance lemmas - they will automtically be", |
111 (cat_lines ["declaration of equivariance lemmas - they will automtically be", |
112 "brought into the form p o c = c"]) #> |
112 "brought into the form p o c = c"]) #> |
113 Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) |
113 Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) |
114 (cat_lines ["declaration of equivariance lemmas - they will will be", |
114 (cat_lines ["declaration of equivariance lemmas - they will will be", |
115 "added/deleted directly to the eqvt thm-list"]) #> |
115 "added/deleted directly to the eqvt thm-list"]) #> |
116 PureThy.add_thms_dynamic (@{binding "eqvt"}, content); |
116 PureThy.add_thms_dynamic (@{binding "eqvts"}, content); |
117 |
117 |
118 |
118 |
119 end; |
119 end; |