src/HOL/Real/RealDef.thy
changeset 25134 3d4953e88449
parent 25112 98824cc791c0
child 25140 273772abbea2
     1.1 --- a/src/HOL/Real/RealDef.thy	Sun Oct 21 14:21:54 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Sun Oct 21 14:53:44 2007 +0200
     1.3 @@ -794,24 +794,24 @@
     1.4  
     1.5  lemma real_of_nat_div2:
     1.6    "0 <= real (n::nat) / real (x) - real (n div x)"
     1.7 -  apply(case_tac "x = 0")
     1.8 -  apply (simp add: neq0_conv)
     1.9 -  apply (simp add: neq0_conv  compare_rls)
    1.10 -  apply (subst real_of_nat_div_aux)
    1.11 -  apply assumption
    1.12 -  apply simp
    1.13 -  apply (subst zero_le_divide_iff)
    1.14 -  apply simp
    1.15 +apply(case_tac "x = 0")
    1.16 + apply (simp)
    1.17 +apply (simp add: compare_rls)
    1.18 +apply (subst real_of_nat_div_aux)
    1.19 + apply simp
    1.20 +apply simp
    1.21 +apply (subst zero_le_divide_iff)
    1.22 +apply simp
    1.23  done
    1.24  
    1.25  lemma real_of_nat_div3:
    1.26    "real (n::nat) / real (x) - real (n div x) <= 1"
    1.27 -  apply(case_tac "x = 0")
    1.28 -  apply (simp add: neq0_conv )
    1.29 -  apply (simp add: compare_rls neq0_conv )
    1.30 -  apply (subst real_of_nat_div_aux)
    1.31 -  apply assumption
    1.32 -  apply simp
    1.33 +apply(case_tac "x = 0")
    1.34 +apply (simp)
    1.35 +apply (simp add: compare_rls)
    1.36 +apply (subst real_of_nat_div_aux)
    1.37 + apply simp
    1.38 +apply simp
    1.39  done
    1.40  
    1.41  lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"