src/HOL/Library/Polynomial.thy
changeset 37770 cddb3106adb8
parent 37765 26bdfb7b680b
child 38857 97775f3e8722
--- a/src/HOL/Library/Polynomial.thy	Mon Jul 12 11:21:56 2010 +0200
+++ b/src/HOL/Library/Polynomial.thy	Mon Jul 12 11:39:27 2010 +0200
@@ -1195,7 +1195,7 @@
     by (rule poly_dvd_antisym)
 qed
 
-interpretation poly_gcd!: abel_semigroup poly_gcd
+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)"