src/HOL/Library/Polynomial.thy
changeset 49962 a8cc904a6820
parent 49834 b27bbb021df1
child 52380 3cc46b8cca5e
     1.1 --- a/src/HOL/Library/Polynomial.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -975,7 +975,7 @@
     1.4    assume "y \<noteq> 0"
     1.5    hence "pdivmod_rel (x + z * y) y (z + x div y) (x mod y)"
     1.6      using pdivmod_rel [of x y]
     1.7 -    by (simp add: pdivmod_rel_def left_distrib)
     1.8 +    by (simp add: pdivmod_rel_def distrib_right)
     1.9    thus "(x + z * y) div y = z + x div y"
    1.10      by (rule div_poly_eq)
    1.11  next