src/HOL/Real/RealDef.thy
changeset 14348 744c868ee0b7
parent 14341 a09441bd4f1e
child 14365 3d4df8c166ae
--- a/src/HOL/Real/RealDef.thy	Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Fri Jan 09 10:46:18 2004 +0100
@@ -825,6 +825,9 @@
 instance real :: ordered_field
 proof
   fix x y z :: real
+  show "0 < (1::real)" 
+    by (force intro: real_gt_zero_preal_Ex [THEN iffD2]
+              simp add: real_one_def real_of_preal_def)
   show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
   show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
   show "\<bar>x\<bar> = (if x < 0 then -x else x)"