src/HOL/Hyperreal/HyperDef.thy
changeset 14348 744c868ee0b7
parent 14341 a09441bd4f1e
child 14361 ad2f5da643b4
--- a/src/HOL/Hyperreal/HyperDef.thy	Fri Jan 09 01:28:24 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Fri Jan 09 10:46:18 2004 +0100
@@ -697,8 +697,12 @@
 instance hypreal :: ordered_field
 proof
   fix x y z :: hypreal
-  show "x \<le> y ==> z + x \<le> z + y" by (rule hypreal_add_left_le_mono1)
-  show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: hypreal_mult_less_mono2)
+  show "0 < (1::hypreal)" 
+    by (unfold hypreal_one_def hypreal_zero_def hypreal_less_def, force)
+  show "x \<le> y ==> z + x \<le> z + y" 
+    by (rule hypreal_add_left_le_mono1)
+  show "x < y ==> 0 < z ==> z * x < z * y" 
+    by (simp add: hypreal_mult_less_mono2)
   show "\<bar>x\<bar> = (if x < 0 then -x else x)"
     by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le)
 qed