--- a/src/HOL/Library/Polynomial.thy Wed Jan 27 14:03:08 2010 +0100
+++ b/src/HOL/Library/Polynomial.thy Thu Jan 28 11:48:43 2010 +0100
@@ -1200,14 +1200,18 @@
by (rule poly_dvd_antisym)
qed
-lemma poly_gcd_commute: "poly_gcd x y = poly_gcd y x"
-by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+interpretation poly_gcd!: abel_semigroup poly_gcd
+proof
+ fix x y z :: "'a poly"
+ show "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
+ by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
+ show "poly_gcd x y = poly_gcd y x"
+ by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic)
+qed
-lemma poly_gcd_assoc: "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"
-by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic)
-
-lemmas poly_gcd_left_commute =
- mk_left_commute [where f=poly_gcd, OF poly_gcd_assoc poly_gcd_commute]
+lemmas poly_gcd_assoc = poly_gcd.assoc
+lemmas poly_gcd_commute = poly_gcd.commute
+lemmas poly_gcd_left_commute = poly_gcd.left_commute
lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute