--- a/src/HOL/Real/RealDef.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Real/RealDef.thy Sun Oct 21 14:53:44 2007 +0200
@@ -794,24 +794,24 @@
lemma real_of_nat_div2:
"0 <= real (n::nat) / real (x) - real (n div x)"
- apply(case_tac "x = 0")
- apply (simp add: neq0_conv)
- apply (simp add: neq0_conv compare_rls)
- apply (subst real_of_nat_div_aux)
- apply assumption
- apply simp
- apply (subst zero_le_divide_iff)
- apply simp
+apply(case_tac "x = 0")
+ apply (simp)
+apply (simp add: compare_rls)
+apply (subst real_of_nat_div_aux)
+ apply simp
+apply simp
+apply (subst zero_le_divide_iff)
+apply simp
done
lemma real_of_nat_div3:
"real (n::nat) / real (x) - real (n div x) <= 1"
- apply(case_tac "x = 0")
- apply (simp add: neq0_conv )
- apply (simp add: compare_rls neq0_conv )
- apply (subst real_of_nat_div_aux)
- apply assumption
- apply simp
+apply(case_tac "x = 0")
+apply (simp)
+apply (simp add: compare_rls)
+apply (subst real_of_nat_div_aux)
+ apply simp
+apply simp
done
lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"