# HG changeset patch
# User huffman
# Date 1234563120 28800
# Node ID 856f16a3b43628de26116fa07b8bb4cc84f5a278
# Parent  333cbcad74c3dda842b4ae74f8447a42b0a9f08a
add class cancel_comm_monoid_add

diff -r 333cbcad74c3 -r 856f16a3b436 src/HOL/NSA/StarDef.thy
--- 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)
diff -r 333cbcad74c3 -r 856f16a3b436 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Feb 13 12:07:03 2009 -0800
+++ b/src/HOL/OrderedGroup.thy	Fri Feb 13 14:12:00 2009 -0800
@@ -147,6 +147,9 @@
 
 end
 
+class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
+
+
 subsection {* Groups *}
 
 class group_add = minus + uminus + monoid_add +
@@ -261,7 +264,7 @@
 subclass group_add
   proof qed (simp_all add: ab_left_minus ab_diff_minus)
 
-subclass cancel_ab_semigroup_add
+subclass cancel_comm_monoid_add
 proof
   fix a b c :: 'a
   assume "a + b = a + c"
diff -r 333cbcad74c3 -r 856f16a3b436 src/HOL/Polynomial.thy
--- a/src/HOL/Polynomial.thy	Fri Feb 13 12:07:03 2009 -0800
+++ b/src/HOL/Polynomial.thy	Fri Feb 13 14:12:00 2009 -0800
@@ -293,8 +293,7 @@
 
 end
 
-instance poly ::
-  ("{cancel_ab_semigroup_add,comm_monoid_add}") cancel_ab_semigroup_add
+instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
 proof
   fix p q r :: "'a poly"
   assume "p + q = p + r" thus "q = r"
diff -r 333cbcad74c3 -r 856f16a3b436 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Fri Feb 13 12:07:03 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Fri Feb 13 14:12:00 2009 -0800
@@ -41,7 +41,7 @@
 
 class semiring_0 = semiring + comm_monoid_add + mult_zero
 
-class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add
+class semiring_0_cancel = semiring + cancel_comm_monoid_add
 begin
 
 subclass semiring_0
@@ -80,7 +80,7 @@
 
 end
 
-class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
+class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
 begin
 
 subclass semiring_0_cancel ..
@@ -198,8 +198,8 @@
 class no_zero_divisors = zero + times +
   assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
 
-class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
-  + cancel_ab_semigroup_add + monoid_mult
+class semiring_1_cancel = semiring + cancel_comm_monoid_add
+  + zero_neq_one + monoid_mult
 begin
 
 subclass semiring_0_cancel ..
@@ -208,8 +208,8 @@
 
 end
 
-class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
-  + zero_neq_one + cancel_ab_semigroup_add
+class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
+  + zero_neq_one + comm_monoid_mult
 begin
 
 subclass semiring_1_cancel ..
@@ -543,7 +543,7 @@
 end
 
 class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
-  + semiring + comm_monoid_add + cancel_ab_semigroup_add
+  + semiring + cancel_comm_monoid_add
 begin
 
 subclass semiring_0_cancel ..