| changeset 54230 | b1d955791529 |
| parent 49962 | a8cc904a6820 |
| child 54489 | 03ff4d1e6784 |
--- a/src/HOL/NSA/StarDef.thy Thu Oct 31 16:54:22 2013 +0100 +++ b/src/HOL/NSA/StarDef.thy Fri Nov 01 18:51:14 2013 +0100 @@ -803,7 +803,7 @@ instance star :: (ab_group_add) ab_group_add apply (intro_classes) apply (transfer, rule left_minus) -apply (transfer, rule diff_minus) +apply (transfer, rule diff_conv_add_uminus) done instance star :: (ordered_ab_semigroup_add) ordered_ab_semigroup_add