src/HOL/Library/Univ_Poly.thy
changeset 28562 4e74209f113e
parent 27487 c8a6ce181805
child 28823 dcbef866c9e2
     1.1 --- a/src/HOL/Library/Univ_Poly.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Library/Univ_Poly.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  
     1.5  definition (in semiring_0)
     1.6    divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "divides" 70) where
     1.7 -  [code func del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
     1.8 +  [code del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
     1.9  
    1.10      --{*order of a polynomial*}
    1.11  definition (in ring_1) order :: "'a => 'a list => nat" where