src/HOL/Library/Polynomial.thy

     using dvd1 dvd2 by (rule poly_gcd_greatest)
   ultimately show ?thesis
     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)
-
-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]
+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
+
+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
 
 lemma poly_gcd_1_left [simp]: "poly_gcd 1 y = 1"
 by (rule poly_gcd_unique) simp_all