src/HOL/Real.thy
changeset 56571 f4635657d66f
parent 56544 b60d5d119489
child 56889 48a745e1bde7
     1.1 --- a/src/HOL/Real.thy	Mon Apr 14 10:55:56 2014 +0200
     1.2 +++ b/src/HOL/Real.thy	Mon Apr 14 13:08:17 2014 +0200
     1.3 @@ -1136,8 +1136,6 @@
     1.4    apply (simp add: algebra_simps)
     1.5    apply (subst real_of_int_div_aux)
     1.6    apply simp
     1.7 -  apply (subst zero_le_divide_iff)
     1.8 -  apply auto
     1.9    apply (simp add: algebra_simps)
    1.10    apply (subst real_of_int_div_aux)
    1.11    apply simp
    1.12 @@ -1269,8 +1267,6 @@
    1.13  apply (simp add: algebra_simps)
    1.14  apply (subst real_of_nat_div_aux)
    1.15  apply simp
    1.16 -apply (subst zero_le_divide_iff)
    1.17 -apply simp
    1.18  done
    1.19  
    1.20  lemma real_of_nat_div3: