1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Fri Jan 09 01:28:24 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Fri Jan 09 10:46:18 2004 +0100
     1.3 @@ -697,8 +697,12 @@
     1.4  instance hypreal :: ordered_field
     1.5  proof
     1.6    fix x y z :: hypreal
     1.7 -  show "x \<le> y ==> z + x \<le> z + y" by (rule hypreal_add_left_le_mono1)
     1.8 -  show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: hypreal_mult_less_mono2)
     1.9 +  show "0 < (1::hypreal)" 
    1.10 +    by (unfold hypreal_one_def hypreal_zero_def hypreal_less_def, force)
    1.11 +  show "x \<le> y ==> z + x \<le> z + y" 
    1.12 +    by (rule hypreal_add_left_le_mono1)
    1.13 +  show "x < y ==> 0 < z ==> z * x < z * y" 
    1.14 +    by (simp add: hypreal_mult_less_mono2)
    1.15    show "\<bar>x\<bar> = (if x < 0 then -x else x)"
    1.16      by (auto dest: order_le_less_trans simp add: hrabs_def linorder_not_le)
    1.17  qed