src/HOL/RComplete.thy
changeset 49962 a8cc904a6820
parent 47596 c031e65c8ddc
child 51518 6a56b7088a6a
     1.1 --- a/src/HOL/RComplete.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/RComplete.thy	Fri Oct 19 15:12:52 2012 +0200
     1.3 @@ -447,7 +447,7 @@
     1.4      done
     1.5    thus "x / real y < real (natfloor x div y) + 1"
     1.6      using assms
     1.7 -    by (simp add: divide_less_eq natfloor_less_iff left_distrib)
     1.8 +    by (simp add: divide_less_eq natfloor_less_iff distrib_right)
     1.9  qed
    1.10  
    1.11  lemma le_mult_natfloor: