| changeset 29904 | 856f16a3b436 |
| parent 29234 | 60f7fb56f8cd |
| child 30198 | 922f944f03b2 |
--- a/src/HOL/NSA/StarDef.thy Fri Feb 13 12:07:03 2009 -0800 +++ b/src/HOL/NSA/StarDef.thy Fri Feb 13 14:12:00 2009 -0800 @@ -844,6 +844,8 @@ instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add by (intro_classes, transfer, rule add_imp_eq) +instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add .. + instance star :: (ab_group_add) ab_group_add apply (intro_classes) apply (transfer, rule left_minus)