src/HOL/Library/Polynomial.thy
changeset 37770 cddb3106adb8
parent 37765 26bdfb7b680b
child 38857 97775f3e8722
     1.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jul 12 11:21:56 2010 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Jul 12 11:39:27 2010 +0200
     1.3 @@ -1195,7 +1195,7 @@
     1.4      by (rule poly_dvd_antisym)
     1.5  qed
     1.6  
     1.7 -interpretation poly_gcd!: abel_semigroup poly_gcd
     1.8 +interpretation poly_gcd: abel_semigroup poly_gcd
     1.9  proof
    1.10    fix x y z :: "'a poly"
    1.11    show "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)"