src/HOL/Real/RealDef.thy
changeset 25112 98824cc791c0
parent 24630 351a308ab58d
child 25134 3d4953e88449
     1.1 --- a/src/HOL/Real/RealDef.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -795,8 +795,8 @@
     1.4  lemma real_of_nat_div2:
     1.5    "0 <= real (n::nat) / real (x) - real (n div x)"
     1.6    apply(case_tac "x = 0")
     1.7 -  apply simp
     1.8 -  apply (simp add: compare_rls)
     1.9 +  apply (simp add: neq0_conv)
    1.10 +  apply (simp add: neq0_conv  compare_rls)
    1.11    apply (subst real_of_nat_div_aux)
    1.12    apply assumption
    1.13    apply simp
    1.14 @@ -807,8 +807,8 @@
    1.15  lemma real_of_nat_div3:
    1.16    "real (n::nat) / real (x) - real (n div x) <= 1"
    1.17    apply(case_tac "x = 0")
    1.18 -  apply simp
    1.19 -  apply (simp add: compare_rls)
    1.20 +  apply (simp add: neq0_conv )
    1.21 +  apply (simp add: compare_rls neq0_conv )
    1.22    apply (subst real_of_nat_div_aux)
    1.23    apply assumption
    1.24    apply simp