changeset 15013 | 34264f5e4691 |
parent 14738 | 83f1a514dcb4 |
child 15055 | aed573241bea |
--- a/src/HOL/Real/PReal.thy Wed Jun 30 14:04:58 2004 +0200 +++ b/src/HOL/Real/PReal.thy Thu Jul 01 12:29:53 2004 +0200 @@ -705,7 +705,7 @@ from preal_nonempty [OF A] show ?case by force case (Suc k) - from this obtain b where "b \<in> A" "b + of_int (int k) * u \<in> A" .. + from this obtain b where "b \<in> A" "b + of_nat k * u \<in> A" .. hence "b + of_int (int k)*u + u \<in> A" by (simp add: prems) thus ?case by (force simp add: left_distrib add_ac prems) qed