--- a/src/HOL/Hyperreal/Integration.thy Sun Oct 21 14:21:54 2007 +0200
+++ b/src/HOL/Hyperreal/Integration.thy Sun Oct 21 14:53:44 2007 +0200
@@ -149,14 +149,13 @@
apply (rule_tac t = a in partition_lhs [THEN subst], assumption)
apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear)
apply (frule partition [THEN iffD1], safe)
-using neq0_conv
apply (blast intro: partition_lt less_le_trans)
apply (rotate_tac 3)
apply (drule_tac x = "Suc n" in spec)
apply (erule impE)
apply (erule less_imp_le)
-apply (frule partition_rhs, simp only: neq0_conv)
-apply (drule partition_gt, assumption)
+apply (frule partition_rhs)
+apply (drule partition_gt[of _ _ _ 0], arith)
apply (simp (no_asm_simp))
done