1.1 --- a/src/HOL/Hyperreal/NSA.ML	Fri Oct 05 23:58:52 2001 +0200
     1.2 +++ b/src/HOL/Hyperreal/NSA.ML	Sat Oct 06 00:02:46 2001 +0200
     1.3 @@ -260,11 +260,11 @@
     1.4  qed "Infinitesimal_zero";
     1.5  AddIffs [Infinitesimal_zero];
     1.6  
     1.7 -Goal "x/(# 2::hypreal) + x/(# 2::hypreal) = x";
     1.8 +Goal "x/(2::hypreal) + x/(2::hypreal) = x";
     1.9  by Auto_tac;  
    1.10  qed "hypreal_sum_of_halves";
    1.11  
    1.12 -Goal "Numeral0 < r ==> Numeral0 < r/(# 2::hypreal)";
    1.13 +Goal "Numeral0 < r ==> Numeral0 < r/(2::hypreal)";
    1.14  by Auto_tac;  
    1.15  qed "hypreal_half_gt_zero";
    1.16