changeset 11704 | 3c50a2cd6f00 |
parent 11701 | 3d51fbf81c17 |
child 12018 | ec054019c910 |
--- a/src/HOL/Hyperreal/NSA.ML Fri Oct 05 23:58:52 2001 +0200 +++ b/src/HOL/Hyperreal/NSA.ML Sat Oct 06 00:02:46 2001 +0200 @@ -260,11 +260,11 @@ qed "Infinitesimal_zero"; AddIffs [Infinitesimal_zero]; -Goal "x/(# 2::hypreal) + x/(# 2::hypreal) = x"; +Goal "x/(2::hypreal) + x/(2::hypreal) = x"; by Auto_tac; qed "hypreal_sum_of_halves"; -Goal "Numeral0 < r ==> Numeral0 < r/(# 2::hypreal)"; +Goal "Numeral0 < r ==> Numeral0 < r/(2::hypreal)"; by Auto_tac; qed "hypreal_half_gt_zero";