| changeset 59815 | cce82e360c2f |
| parent 59680 | 034a4d15b52e |
| child 59816 | 034b13f4efae |
--- a/src/HOL/NSA/StarDef.thy Mon Mar 23 19:05:14 2015 +0100 +++ b/src/HOL/NSA/StarDef.thy Mon Mar 23 19:05:14 2015 +0100 @@ -795,7 +795,7 @@ done instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add -by (intro_classes, transfer, rule add_left_imp_eq) +by intro_classes (transfer, simp add: diff_diff_eq)+ instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..