(*f -> ( *f because of new comments
authornipkow
Fri Feb 07 16:40:23 2003 +0100 (2003-02-07)
changeset 13810c3fbfd472365
parent 13809 a4cd9057d2ee
child 13811 f39f67982854
(*f -> ( *f because of new comments
src/HOL/Hyperreal/ExtraThms2.ML
src/HOL/Hyperreal/HSeries.ML
src/HOL/Hyperreal/Lim.ML
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/NatStar.ML
src/HOL/Hyperreal/SEQ.ML
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Star.ML
     1.1 --- a/src/HOL/Hyperreal/ExtraThms2.ML	Fri Feb 07 15:36:54 2003 +0100
     1.2 +++ b/src/HOL/Hyperreal/ExtraThms2.ML	Fri Feb 07 16:40:23 2003 +0100
     1.3 @@ -498,7 +498,7 @@
     1.4  Addsimps [HNatInfinite_inverse_not_zero];
     1.5  
     1.6  Goal "N : HNatInfinite \
     1.7 -\     ==> (*fNat* (%x. inverse (real x))) N : Infinitesimal";
     1.8 +\     ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal";
     1.9  by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
    1.10  by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
    1.11  by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat]));
     2.1 --- a/src/HOL/Hyperreal/HSeries.ML	Fri Feb 07 15:36:54 2003 +0100
     2.2 +++ b/src/HOL/Hyperreal/HSeries.ML	Fri Feb 07 16:40:23 2003 +0100
     2.3 @@ -45,7 +45,7 @@
     2.4  (* Theorem corresponding to recursive case in def of sumr *)
     2.5  Goalw [hypnat_one_def]
     2.6       "sumhr(m,n+(1::hypnat),f) = (if n + (1::hypnat) <= m then 0 \
     2.7 -\                         else sumhr(m,n,f) + (*fNat* f) n)";
     2.8 +\                         else sumhr(m,n,f) + ( *fNat* f) n)";
     2.9  by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
    2.10  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
    2.11  by (auto_tac (claset(),
    2.12 @@ -68,7 +68,7 @@
    2.13  Addsimps [sumhr_eq_bounds];
    2.14  
    2.15  Goalw [hypnat_one_def] 
    2.16 -     "sumhr (m,m + (1::hypnat),f) = (*fNat* f) m";
    2.17 +     "sumhr (m,m + (1::hypnat),f) = ( *fNat* f) m";
    2.18  by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
    2.19  by (auto_tac (claset(),
    2.20                simpset() addsimps [sumhr, hypnat_add,starfunNat]));
    2.21 @@ -206,7 +206,7 @@
    2.22  qed "sumhr_interval_const";
    2.23  
    2.24  Goalw [hypnat_zero_def]
    2.25 -     "(*fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)";
    2.26 +     "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)";
    2.27  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
    2.28  by (asm_full_simp_tac (simpset() addsimps [starfunNat,sumhr]) 1);
    2.29  qed "starfunNat_sumr";
     3.1 --- a/src/HOL/Hyperreal/Lim.ML	Fri Feb 07 15:36:54 2003 +0100
     3.2 +++ b/src/HOL/Hyperreal/Lim.ML	Fri Feb 07 16:40:23 2003 +0100
     3.3 @@ -438,7 +438,7 @@
     3.4  
     3.5  Goalw [isNSCont_def] 
     3.6        "[| isNSCont f a; y \\<approx> hypreal_of_real a |] \
     3.7 -\           ==> (*f* f) y \\<approx> hypreal_of_real (f a)";
     3.8 +\           ==> ( *f* f) y \\<approx> hypreal_of_real (f a)";
     3.9  by (Blast_tac 1);
    3.10  qed "isNSContD";
    3.11  
    3.12 @@ -662,7 +662,7 @@
    3.13                          Uniform continuity
    3.14   ------------------------------------------------------------------*)
    3.15  Goalw [isNSUCont_def] 
    3.16 -      "[| isNSUCont f; x \\<approx> y|] ==> (*f* f) x \\<approx> (*f* f) y";
    3.17 +      "[| isNSUCont f; x \\<approx> y|] ==> ( *f* f) x \\<approx> ( *f* f) y";
    3.18  by (Blast_tac 1);
    3.19  qed "isNSUContD";
    3.20  
    3.21 @@ -859,7 +859,7 @@
    3.22       "(NSDERIV f x :> D) = \
    3.23  \     (\\<forall>xa. \
    3.24  \       xa \\<noteq> hypreal_of_real x & xa \\<approx> hypreal_of_real x --> \
    3.25 -\       (*f* (%z. (f z - f x) / (z - x))) xa \\<approx> hypreal_of_real D)";
    3.26 +\       ( *f* (%z. (f z - f x) / (z - x))) xa \\<approx> hypreal_of_real D)";
    3.27  by (auto_tac (claset(), simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def]));
    3.28  qed "NSDERIV_iff2";
    3.29  
    3.30 @@ -867,7 +867,7 @@
    3.31  Goal "(NSDERIV f x :> D) ==> \
    3.32  \    (\\<forall>u. \
    3.33  \       u \\<approx> hypreal_of_real x --> \
    3.34 -\       (*f* (%z. f z - f x)) u \\<approx> hypreal_of_real D * (u - hypreal_of_real x))";
    3.35 +\       ( *f* (%z. f z - f x)) u \\<approx> hypreal_of_real D * (u - hypreal_of_real x))";
    3.36  by (auto_tac (claset(), simpset() addsimps [NSDERIV_iff2]));
    3.37  by (case_tac "u = hypreal_of_real x" 1);
    3.38  by (auto_tac (claset(), simpset() addsimps [hypreal_diff_def]));
    3.39 @@ -876,7 +876,7 @@
    3.40  by (dres_inst_tac [("c","u - hypreal_of_real x"),("b","hypreal_of_real D")]
    3.41       approx_mult1 1);
    3.42  by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1)));
    3.43 -by (subgoal_tac "(*f* (%z. z - x)) u \\<noteq> (0::hypreal)" 2);
    3.44 +by (subgoal_tac "( *f* (%z. z - x)) u \\<noteq> (0::hypreal)" 2);
    3.45  by (auto_tac (claset(),
    3.46      simpset() addsimps [real_diff_def, hypreal_diff_def, 
    3.47  		(approx_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),  
    3.48 @@ -885,7 +885,7 @@
    3.49  
    3.50  Goal "(NSDERIV f x :> D) ==> \
    3.51  \     (\\<forall>h \\<in> Infinitesimal. \
    3.52 -\              ((*f* f)(hypreal_of_real x + h) - \
    3.53 +\              (( *f* f)(hypreal_of_real x + h) - \
    3.54  \                hypreal_of_real (f x))\\<approx> (hypreal_of_real D) * h)";
    3.55  by (auto_tac (claset(),simpset() addsimps [nsderiv_def]));
    3.56  by (case_tac "h = (0::hypreal)" 1);
    3.57 @@ -898,7 +898,7 @@
    3.58  
    3.59  Goal "(NSDERIV f x :> D) ==> \
    3.60  \     (\\<forall>h \\<in> Infinitesimal - {0}. \
    3.61 -\              ((*f* f)(hypreal_of_real x + h) - \
    3.62 +\              (( *f* f)(hypreal_of_real x + h) - \
    3.63  \                hypreal_of_real (f x))\\<approx> (hypreal_of_real D) * h)";
    3.64  by (auto_tac (claset(),simpset() addsimps [nsderiv_def]));
    3.65  by (rtac ccontr 1 THEN dres_inst_tac [("x","h")] bspec 1);
    3.66 @@ -1114,13 +1114,13 @@
    3.67   ---------------------------------------------------------------*)
    3.68  Goalw [increment_def] 
    3.69        "f NSdifferentiable x ==> \
    3.70 -\     increment f x h = (*f* f) (hypreal_of_real(x) + h) + \
    3.71 +\     increment f x h = ( *f* f) (hypreal_of_real(x) + h) + \
    3.72  \     -hypreal_of_real (f x)";
    3.73  by (Blast_tac 1);
    3.74  qed "incrementI";
    3.75  
    3.76  Goal "NSDERIV f x :> D ==> \
    3.77 -\    increment f x h = (*f* f) (hypreal_of_real(x) + h) + \
    3.78 +\    increment f x h = ( *f* f) (hypreal_of_real(x) + h) + \
    3.79  \    -hypreal_of_real (f x)";
    3.80  by (etac (NSdifferentiableI RS incrementI) 1);
    3.81  qed "incrementI2";
    3.82 @@ -1133,7 +1133,7 @@
    3.83  by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1 THEN Step_tac 1);
    3.84  by (forw_inst_tac [("b1","hypreal_of_real(D) + y")] 
    3.85      ((hypreal_mult_right_cancel RS iffD2)) 1);
    3.86 -by (thin_tac "((*f* f) (hypreal_of_real(x) + h) + \
    3.87 +by (thin_tac "(( *f* f) (hypreal_of_real(x) + h) + \
    3.88  \   - hypreal_of_real (f x)) / h = hypreal_of_real(D) + y" 2);
    3.89  by (assume_tac 1);
    3.90  by (asm_full_simp_tac (simpset() addsimps [hypreal_times_divide1_eq RS sym]
    3.91 @@ -1169,7 +1169,7 @@
    3.92  (* lemmas *)
    3.93  Goalw [nsderiv_def] 
    3.94        "[| NSDERIV g x :> D; \
    3.95 -\              (*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\
    3.96 +\              ( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\
    3.97  \              xa \\<in> Infinitesimal;\
    3.98  \              xa \\<noteq> 0 \
    3.99  \           |] ==> D = 0";
   3.100 @@ -1180,7 +1180,7 @@
   3.101  (* can be proved differently using NSLIM_isCont_iff *)
   3.102  Goalw [nsderiv_def] 
   3.103       "[| NSDERIV f x :> D;  h \\<in> Infinitesimal;  h \\<noteq> 0 |]  \
   3.104 -\     ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> 0";    
   3.105 +\     ==> ( *f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) \\<approx> 0";    
   3.106  by (asm_full_simp_tac (simpset() addsimps 
   3.107      [mem_infmal_iff RS sym]) 1);
   3.108  by (rtac Infinitesimal_ratio 1);
   3.109 @@ -1196,11 +1196,11 @@
   3.110                    x - a
   3.111   ---------------------------------------------------------------*)
   3.112  Goal "[| NSDERIV f (g x) :> Da; \
   3.113 -\        (*f* g) (hypreal_of_real(x) + xa) \\<noteq> hypreal_of_real (g x); \
   3.114 -\        (*f* g) (hypreal_of_real(x) + xa) \\<approx> hypreal_of_real (g x) \
   3.115 -\     |] ==> ((*f* f) ((*f* g) (hypreal_of_real(x) + xa)) \
   3.116 +\        ( *f* g) (hypreal_of_real(x) + xa) \\<noteq> hypreal_of_real (g x); \
   3.117 +\        ( *f* g) (hypreal_of_real(x) + xa) \\<approx> hypreal_of_real (g x) \
   3.118 +\     |] ==> (( *f* f) (( *f* g) (hypreal_of_real(x) + xa)) \
   3.119  \                  + - hypreal_of_real (f (g x))) \
   3.120 -\             / ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) \
   3.121 +\             / (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) \
   3.122  \            \\<approx> hypreal_of_real(Da)";
   3.123  by (auto_tac (claset(),
   3.124         simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def]));
   3.125 @@ -1214,7 +1214,7 @@
   3.126                         h
   3.127   --------------------------------------------------------------*)
   3.128  Goal "[| NSDERIV g x :> Db; xa \\<in> Infinitesimal; xa \\<noteq> 0 |] \
   3.129 -\     ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
   3.130 +\     ==> (( *f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
   3.131  \         \\<approx> hypreal_of_real(Db)";
   3.132  by (auto_tac (claset(),
   3.133      simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def, 
   3.134 @@ -1235,10 +1235,10 @@
   3.135  by (forw_inst_tac [("f","g")] NSDERIV_approx 1);
   3.136  by (auto_tac (claset(),
   3.137                simpset() addsimps [starfun_lambda_cancel2, starfun_o RS sym]));
   3.138 -by (case_tac "(*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1);
   3.139 +by (case_tac "( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1);
   3.140  by (dres_inst_tac [("g","g")] NSDERIV_zero 1);
   3.141  by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def]));
   3.142 -by (res_inst_tac [("z1","(*f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"),
   3.143 +by (res_inst_tac [("z1","( *f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"),
   3.144      ("y1","inverse xa")] (lemma_chain RS ssubst) 1);
   3.145  by (etac (hypreal_not_eq_minus_iff RS iffD1) 1);
   3.146  by (rtac approx_mult_hypreal_of_real 1);
     4.1 --- a/src/HOL/Hyperreal/Lim.thy	Fri Feb 07 15:36:54 2003 +0100
     4.2 +++ b/src/HOL/Hyperreal/Lim.thy	Fri Feb 07 16:40:23 2003 +0100
     4.3 @@ -23,7 +23,7 @@
     4.4  			      ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
     4.5    "f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a & 
     4.6  		      x @= hypreal_of_real a -->
     4.7 -		      (*f* f) x @= hypreal_of_real L))"   
     4.8 +		      ( *f* f) x @= hypreal_of_real L))"   
     4.9  
    4.10    isCont :: [real=>real,real] => bool
    4.11    "isCont f a == (f -- a --> (f a))"        
    4.12 @@ -31,7 +31,7 @@
    4.13    (* NS definition dispenses with limit notions *)
    4.14    isNSCont :: [real=>real,real] => bool
    4.15    "isNSCont f a == (ALL y. y @= hypreal_of_real a --> 
    4.16 -			   (*f* f) y @= hypreal_of_real (f a))"
    4.17 +			   ( *f* f) y @= hypreal_of_real (f a))"
    4.18  
    4.19    (* differentiation: D is derivative of function f at x *)
    4.20    deriv:: [real=>real,real,real] => bool
    4.21 @@ -41,7 +41,7 @@
    4.22    nsderiv :: [real=>real,real,real] => bool
    4.23  			    ("(NSDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
    4.24    "NSDERIV f x :> D == (ALL h: Infinitesimal - {0}. 
    4.25 -			((*f* f)(hypreal_of_real x + h) + 
    4.26 +			(( *f* f)(hypreal_of_real x + h) + 
    4.27  			 - hypreal_of_real (f x))/h @= hypreal_of_real D)"
    4.28  
    4.29    differentiable :: [real=>real,real] => bool   (infixl 60)
    4.30 @@ -52,7 +52,7 @@
    4.31  
    4.32    increment :: [real=>real,real,hypreal] => hypreal
    4.33    "increment f x h == (@inc. f NSdifferentiable x & 
    4.34 -		       inc = (*f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
    4.35 +		       inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
    4.36  
    4.37    isUCont :: (real=>real) => bool
    4.38    "isUCont f ==  (ALL r. 0 < r --> 
    4.39 @@ -60,7 +60,7 @@
    4.40  			    --> abs(f x + -f y) < r)))"
    4.41  
    4.42    isNSUCont :: (real=>real) => bool
    4.43 -  "isNSUCont f == (ALL x y. x @= y --> (*f* f) x @= (*f* f) y)"
    4.44 +  "isNSUCont f == (ALL x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
    4.45  
    4.46  
    4.47  (*Used in the proof of the Bolzano theorem*)
     5.1 --- a/src/HOL/Hyperreal/NatStar.ML	Fri Feb 07 15:36:54 2003 +0100
     5.2 +++ b/src/HOL/Hyperreal/NatStar.ML	Fri Feb 07 16:40:23 2003 +0100
     5.3 @@ -70,7 +70,7 @@
     5.4           simpset() addsimps [starsetNat_n_Int RS sym]));
     5.5  qed "InternalNatSets_Int";
     5.6  
     5.7 -Goalw [starsetNat_def] "*sNat* (-A) = -(*sNat* A)";
     5.8 +Goalw [starsetNat_def] "*sNat* (-A) = -( *sNat* A)";
     5.9  by (Auto_tac);
    5.10  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    5.11  by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
    5.12 @@ -78,7 +78,7 @@
    5.13  by (TRYALL(Ultra_tac));
    5.14  qed "NatStar_Compl";
    5.15  
    5.16 -Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -(*sNatn* A)";
    5.17 +Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -( *sNatn* A)";
    5.18  by (Auto_tac);
    5.19  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    5.20  by (res_inst_tac [("z","x")] eq_Abs_hypnat 2);
    5.21 @@ -148,7 +148,7 @@
    5.22  by Auto_tac;
    5.23  qed "starsetNat_starsetNat_n_eq";
    5.24  
    5.25 -Goalw [InternalNatSets_def] "(*sNat* X) : InternalNatSets";
    5.26 +Goalw [InternalNatSets_def] "( *sNat* X) : InternalNatSets";
    5.27  by (auto_tac (claset(),
    5.28           simpset() addsimps [starsetNat_starsetNat_n_eq]));
    5.29  qed "InternalNatSets_starsetNat_n";
    5.30 @@ -195,7 +195,7 @@
    5.31  
    5.32  (* f::nat=>real *)
    5.33  Goalw [starfunNat_def]
    5.34 -      "(*fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
    5.35 +      "( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
    5.36  \      Abs_hypreal(hyprel `` {%n. f (X n)})";
    5.37  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
    5.38  by (simp_tac (simpset() addsimps 
    5.39 @@ -205,7 +205,7 @@
    5.40  
    5.41  (* f::nat=>nat *)
    5.42  Goalw [starfunNat2_def]
    5.43 -      "(*fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
    5.44 +      "( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
    5.45  \      Abs_hypnat(hypnatrel `` {%n. f (X n)})";
    5.46  by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1);
    5.47  by (simp_tac (simpset() addsimps 
    5.48 @@ -216,12 +216,12 @@
    5.49  (*---------------------------------------------
    5.50    multiplication: ( *f ) x ( *g ) = *(f x g)  
    5.51   ---------------------------------------------*)
    5.52 -Goal "(*fNat* f) z * (*fNat* g) z = (*fNat* (%x. f x * g x)) z";
    5.53 +Goal "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z";
    5.54  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
    5.55  by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_mult]));
    5.56  qed "starfunNat_mult";
    5.57  
    5.58 -Goal "(*fNat2* f) z * (*fNat2* g) z = (*fNat2* (%x. f x * g x)) z";
    5.59 +Goal "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z";
    5.60  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
    5.61  by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_mult]));
    5.62  qed "starfunNat2_mult";
    5.63 @@ -229,17 +229,17 @@
    5.64  (*---------------------------------------
    5.65    addition: ( *f ) + ( *g ) = *(f + g)  
    5.66   ---------------------------------------*)
    5.67 -Goal "(*fNat* f) z + (*fNat* g) z = (*fNat* (%x. f x + g x)) z";
    5.68 +Goal "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z";
    5.69  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
    5.70  by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_add]));
    5.71  qed "starfunNat_add";
    5.72  
    5.73 -Goal "(*fNat2* f) z + (*fNat2* g) z = (*fNat2* (%x. f x + g x)) z";
    5.74 +Goal "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z";
    5.75  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
    5.76  by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_add]));
    5.77  qed "starfunNat2_add";
    5.78  
    5.79 -Goal "(*fNat2* f) z - (*fNat2* g) z = (*fNat2* (%x. f x - g x)) z";
    5.80 +Goal "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z";
    5.81  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
    5.82  by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_minus]));
    5.83  qed "starfunNat2_minus";
    5.84 @@ -249,18 +249,18 @@
    5.85   ---------------------------------------*)
    5.86  (***** ( *f::nat=>real ) o ( *g::nat=>nat ) = *(f o g) *****)
    5.87   
    5.88 -Goal "(*fNat* f) o (*fNat2* g) = (*fNat* (f o g))";
    5.89 +Goal "( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))";
    5.90  by (rtac ext 1);
    5.91  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
    5.92  by (auto_tac (claset(), simpset() addsimps [starfunNat2, starfunNat]));
    5.93  qed "starfunNatNat2_o";
    5.94  
    5.95 -Goal "(%x. (*fNat* f) ((*fNat2* g) x)) = (*fNat* (%x. f(g x)))";
    5.96 +Goal "(%x. ( *fNat* f) (( *fNat2* g) x)) = ( *fNat* (%x. f(g x)))";
    5.97  by (rtac ( simplify (simpset() addsimps [o_def]) starfunNatNat2_o) 1);
    5.98  qed "starfunNatNat2_o2";
    5.99  
   5.100  (***** ( *f::nat=>nat ) o ( *g::nat=>nat ) = *(f o g) *****)
   5.101 -Goal "(*fNat2* f) o (*fNat2* g) = (*fNat2* (f o g))";
   5.102 +Goal "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))";
   5.103  by (rtac ext 1);
   5.104  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   5.105  by (auto_tac (claset(), simpset() addsimps [starfunNat2]));
   5.106 @@ -268,38 +268,38 @@
   5.107  
   5.108  (***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****)
   5.109  
   5.110 -Goal "(*f* f) o (*fNat* g) = (*fNat* (f o g))"; 
   5.111 +Goal "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))"; 
   5.112  by (rtac ext 1);
   5.113  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   5.114  by (auto_tac (claset(), simpset() addsimps [starfunNat,starfun]));
   5.115  qed "starfun_stafunNat_o";
   5.116  
   5.117 -Goal "(%x. (*f* f) ((*fNat* g) x)) = (*fNat* (%x. f (g x)))"; 
   5.118 +Goal "(%x. ( *f* f) (( *fNat* g) x)) = ( *fNat* (%x. f (g x)))"; 
   5.119  by (rtac ( simplify (simpset() addsimps [o_def]) starfun_stafunNat_o) 1);
   5.120  qed "starfun_stafunNat_o2";
   5.121  
   5.122  (*--------------------------------------
   5.123    NS extension of constant function
   5.124   --------------------------------------*)
   5.125 -Goal "(*fNat* (%x. k)) z = hypreal_of_real k";
   5.126 +Goal "( *fNat* (%x. k)) z = hypreal_of_real k";
   5.127  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   5.128  by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_of_real_def]));
   5.129  qed "starfunNat_const_fun";
   5.130  Addsimps [starfunNat_const_fun];
   5.131  
   5.132 -Goal "(*fNat2* (%x. k)) z = hypnat_of_nat  k";
   5.133 +Goal "( *fNat2* (%x. k)) z = hypnat_of_nat  k";
   5.134  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   5.135  by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def]));
   5.136  qed "starfunNat2_const_fun";
   5.137  
   5.138  Addsimps [starfunNat2_const_fun];
   5.139  
   5.140 -Goal "- (*fNat* f) x = (*fNat* (%x. - f x)) x";
   5.141 +Goal "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x";
   5.142  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   5.143  by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_minus]));
   5.144  qed "starfunNat_minus";
   5.145  
   5.146 -Goal "inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x";
   5.147 +Goal "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x";
   5.148  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   5.149  by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_inverse]));
   5.150  qed "starfunNat_inverse";
   5.151 @@ -310,20 +310,20 @@
   5.152     for all natural arguments (c.f. Hoskins pg. 107- SEQ)
   5.153   -------------------------------------------------------*)
   5.154  
   5.155 -Goal "(*fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
   5.156 +Goal "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
   5.157  by (auto_tac (claset(),
   5.158        simpset() addsimps [starfunNat,hypnat_of_nat_def,hypreal_of_real_def]));
   5.159  qed "starfunNat_eq";
   5.160  
   5.161  Addsimps [starfunNat_eq];
   5.162  
   5.163 -Goal "(*fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
   5.164 +Goal "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
   5.165  by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def]));
   5.166  qed "starfunNat2_eq";
   5.167  
   5.168  Addsimps [starfunNat2_eq];
   5.169  
   5.170 -Goal "(*fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)";
   5.171 +Goal "( *fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)";
   5.172  by (Auto_tac);
   5.173  qed "starfunNat_approx";
   5.174  
   5.175 @@ -333,7 +333,7 @@
   5.176      --- used for limit comparison of sequences
   5.177   ----------------------------------------------------------------*)
   5.178  Goal "ALL n. N <= n --> f n <= g n \
   5.179 -\         ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n <= (*fNat* g) n";
   5.180 +\         ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n <= ( *fNat* g) n";
   5.181  by (Step_tac 1);
   5.182  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   5.183  by (auto_tac (claset(),
   5.184 @@ -345,7 +345,7 @@
   5.185  
   5.186  (*****----- and another -----*****) 
   5.187  Goal "ALL n. N <= n --> f n < g n \
   5.188 -\         ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n < (*fNat* g) n";
   5.189 +\         ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n < ( *fNat* g) n";
   5.190  by (Step_tac 1);
   5.191  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   5.192  by (auto_tac (claset(),
   5.193 @@ -358,7 +358,7 @@
   5.194  (*----------------------------------------------------------------
   5.195              NS extension when we displace argument by one
   5.196   ---------------------------------------------------------------*)
   5.197 -Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + (1::hypnat))";
   5.198 +Goal "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))";
   5.199  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   5.200  by (auto_tac (claset(),
   5.201           simpset() addsimps [starfunNat, hypnat_one_def,hypnat_add]));
   5.202 @@ -367,7 +367,7 @@
   5.203  (*----------------------------------------------------------------
   5.204                   NS extension with rabs    
   5.205   ---------------------------------------------------------------*)
   5.206 -Goal "(*fNat* (%n. abs (f n))) N = abs((*fNat* f) N)";
   5.207 +Goal "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)";
   5.208  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   5.209  by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_hrabs]));
   5.210  qed "starfunNat_rabs";
   5.211 @@ -375,19 +375,19 @@
   5.212  (*----------------------------------------------------------------
   5.213         The hyperpow function as a NS extension of realpow
   5.214   ----------------------------------------------------------------*)
   5.215 -Goal "(*fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N";
   5.216 +Goal "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N";
   5.217  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   5.218  by (auto_tac (claset(),
   5.219           simpset() addsimps [hyperpow, hypreal_of_real_def,starfunNat]));
   5.220  qed "starfunNat_pow";
   5.221  
   5.222 -Goal "(*fNat* (%n. (X n) ^ m)) N = (*fNat* X) N pow hypnat_of_nat m";
   5.223 +Goal "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m";
   5.224  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
   5.225  by (auto_tac (claset(),
   5.226           simpset() addsimps [hyperpow, hypnat_of_nat_def,starfunNat]));
   5.227  qed "starfunNat_pow2";
   5.228  
   5.229 -Goalw [hypnat_of_nat_def] "(*f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
   5.230 +Goalw [hypnat_of_nat_def] "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
   5.231  by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   5.232  by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun]));
   5.233  qed "starfun_pow";
   5.234 @@ -395,14 +395,14 @@
   5.235  (*----------------------------------------------------- 
   5.236     hypreal_of_hypnat as NS extension of real (from "nat")! 
   5.237  -------------------------------------------------------*)
   5.238 -Goal "(*fNat* real) = hypreal_of_hypnat";
   5.239 +Goal "( *fNat* real) = hypreal_of_hypnat";
   5.240  by (rtac ext 1);
   5.241  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   5.242  by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat,starfunNat]));
   5.243  qed "starfunNat_real_of_nat";
   5.244  
   5.245  Goal "N : HNatInfinite \
   5.246 -\  ==> (*fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)";
   5.247 +\  ==> ( *fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)";
   5.248  by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
   5.249  by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
   5.250  by (auto_tac (claset(), 
   5.251 @@ -419,7 +419,7 @@
   5.252  qed "starfunNat_n_congruent";
   5.253  
   5.254  Goalw [starfunNat_n_def]
   5.255 -     "(*fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
   5.256 +     "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \
   5.257  \     Abs_hypreal(hyprel `` {%n. f n (X n)})";
   5.258  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   5.259  by Auto_tac;
   5.260 @@ -429,7 +429,7 @@
   5.261  (*-------------------------------------------------
   5.262    multiplication: ( *fn ) x ( *gn ) = *(fn x gn)  
   5.263   -------------------------------------------------*)
   5.264 -Goal "(*fNatn* f) z * (*fNatn* g) z = (*fNatn* (% i x. f i x * g i x)) z";
   5.265 +Goal "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z";
   5.266  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   5.267  by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_mult]));
   5.268  qed "starfunNat_n_mult";
   5.269 @@ -437,7 +437,7 @@
   5.270  (*-----------------------------------------------
   5.271    addition: ( *fn ) + ( *gn ) = *(fn + gn)  
   5.272   -----------------------------------------------*)
   5.273 -Goal "(*fNatn* f) z + (*fNatn* g) z = (*fNatn* (%i x. f i x + g i x)) z";
   5.274 +Goal "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z";
   5.275  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   5.276  by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_add]));
   5.277  qed "starfunNat_n_add";
   5.278 @@ -445,7 +445,7 @@
   5.279  (*-------------------------------------------------
   5.280    subtraction: ( *fn ) + -( *gn ) = *(fn + -gn)  
   5.281   -------------------------------------------------*)
   5.282 -Goal "(*fNatn* f) z + -(*fNatn* g) z = (*fNatn* (%i x. f i x + -g i x)) z";
   5.283 +Goal "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z";
   5.284  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   5.285  by (auto_tac (claset(), 
   5.286            simpset() addsimps [starfunNat_n, hypreal_minus,hypreal_add]));
   5.287 @@ -455,7 +455,7 @@
   5.288    composition: ( *fn ) o ( *gn ) = *(fn o gn)  
   5.289   -------------------------------------------------*)
   5.290   
   5.291 -Goal "(*fNatn* (%i x. k)) z = hypreal_of_real  k";
   5.292 +Goal "( *fNatn* (%i x. k)) z = hypreal_of_real  k";
   5.293  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   5.294  by (auto_tac (claset(), 
   5.295         simpset() addsimps [starfunNat_n, hypreal_of_real_def]));
   5.296 @@ -463,17 +463,17 @@
   5.297  
   5.298  Addsimps [starfunNat_n_const_fun];
   5.299  
   5.300 -Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x";
   5.301 +Goal "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x";
   5.302  by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   5.303  by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus]));
   5.304  qed "starfunNat_n_minus";
   5.305  
   5.306 -Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
   5.307 +Goal "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
   5.308  by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
   5.309  qed "starfunNat_n_eq";
   5.310  Addsimps [starfunNat_n_eq];
   5.311  
   5.312 -Goal "((*fNat* f) = (*fNat* g)) = (f = g)";
   5.313 +Goal "(( *fNat* f) = ( *fNat* g)) = (f = g)";
   5.314  by Auto_tac;
   5.315  by (rtac ext 1 THEN rtac ccontr 1);
   5.316  by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);
     6.1 --- a/src/HOL/Hyperreal/SEQ.ML	Fri Feb 07 15:36:54 2003 +0100
     6.2 +++ b/src/HOL/Hyperreal/SEQ.ML	Fri Feb 07 16:40:23 2003 +0100
     6.3 @@ -11,7 +11,7 @@
     6.4   -------------------------------------------------------------------------- *)
     6.5  
     6.6  Goalw [hypnat_omega_def] 
     6.7 -      "(*fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal";
     6.8 +      "( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal";
     6.9  by (auto_tac (claset(),
    6.10        simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat]));
    6.11  by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    6.12 @@ -31,7 +31,7 @@
    6.13  qed "LIMSEQ_iff";
    6.14  
    6.15  Goalw [NSLIMSEQ_def] 
    6.16 -    "(X ----NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)";
    6.17 +    "(X ----NS> L) = (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)";
    6.18  by (Simp_tac 1);
    6.19  qed "NSLIMSEQ_iff";
    6.20  
    6.21 @@ -121,7 +121,7 @@
    6.22  val lemmaLIM2 = result();
    6.23  
    6.24  Goal "[| 0 < r; ALL n. r <= abs (X (f n) + - L); \
    6.25 -\          (*fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \
    6.26 +\          ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \
    6.27  \          - hypreal_of_real  L @= 0 |] ==> False";
    6.28  by (auto_tac (claset(),simpset() addsimps [starfunNat,
    6.29      mem_infmal_iff RS sym,hypreal_of_real_def,
    6.30 @@ -419,12 +419,12 @@
    6.31  qed "Bseq_iff1a";
    6.32  
    6.33  Goalw [NSBseq_def]
    6.34 -     "[| NSBseq X;  N: HNatInfinite |] ==> (*fNat* X) N : HFinite";
    6.35 +     "[| NSBseq X;  N: HNatInfinite |] ==> ( *fNat* X) N : HFinite";
    6.36  by (Blast_tac 1);
    6.37  qed "NSBseqD";
    6.38  
    6.39  Goalw [NSBseq_def]
    6.40 -     "ALL N: HNatInfinite. (*fNat* X) N : HFinite ==> NSBseq X";
    6.41 +     "ALL N: HNatInfinite. ( *fNat* X) N : HFinite ==> NSBseq X";
    6.42  by (assume_tac 1);
    6.43  qed "NSBseqI";
    6.44  
     7.1 --- a/src/HOL/Hyperreal/SEQ.thy	Fri Feb 07 15:36:54 2003 +0100
     7.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Fri Feb 07 16:40:23 2003 +0100
     7.3 @@ -14,7 +14,7 @@
     7.4    
     7.5    (* Nonstandard definition of convergence of sequence *)
     7.6    NSLIMSEQ :: [nat=>real,real] => bool    ("((_)/ ----NS> (_))" [60, 60] 60)
     7.7 -  "X ----NS> L == (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)"
     7.8 +  "X ----NS> L == (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)"
     7.9  
    7.10    (* define value of limit using choice operator*)
    7.11    lim :: (nat => real) => real
    7.12 @@ -37,7 +37,7 @@
    7.13   
    7.14    (* Nonstandard definition for bounded sequence *)
    7.15    NSBseq :: (nat=>real) => bool
    7.16 -  "NSBseq X == (ALL N: HNatInfinite. (*fNat* X) N : HFinite)" 
    7.17 +  "NSBseq X == (ALL N: HNatInfinite. ( *fNat* X) N : HFinite)" 
    7.18  
    7.19    (* Definition for monotonicity *)
    7.20    monoseq :: (nat=>real)=>bool
    7.21 @@ -58,6 +58,6 @@
    7.22  
    7.23    NSCauchy :: (nat => real) => bool
    7.24    "NSCauchy X == (ALL M: HNatInfinite. ALL N: HNatInfinite.
    7.25 -                      (*fNat* X) M @= (*fNat* X) N)"
    7.26 +                      ( *fNat* X) M @= ( *fNat* X) N)"
    7.27  end
    7.28  
     8.1 --- a/src/HOL/Hyperreal/Star.ML	Fri Feb 07 15:36:54 2003 +0100
     8.2 +++ b/src/HOL/Hyperreal/Star.ML	Fri Feb 07 16:40:23 2003 +0100
     8.3 @@ -51,7 +51,7 @@
     8.4  by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
     8.5  qed "STAR_Int";
     8.6  
     8.7 -Goalw [starset_def] "*s* -A = -(*s* A)";
     8.8 +Goalw [starset_def] "*s* -A = -( *s* A)";
     8.9  by (Auto_tac);
    8.10  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    8.11  by (res_inst_tac [("z","x")] eq_Abs_hypreal 2);
    8.12 @@ -198,7 +198,7 @@
    8.13  qed "starfun_congruent";
    8.14  
    8.15  Goalw [starfun_def]
    8.16 -      "(*f* f) (Abs_hypreal(hyprel``{%n. X n})) = \
    8.17 +      "( *f* f) (Abs_hypreal(hyprel``{%n. X n})) = \
    8.18  \      Abs_hypreal(hyprel `` {%n. f (X n)})";
    8.19  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
    8.20  by (simp_tac (simpset() addsimps 
    8.21 @@ -209,7 +209,7 @@
    8.22  (*-------------------------------------------
    8.23    multiplication: ( *f ) x ( *g ) = *(f x g)  
    8.24   ------------------------------------------*)
    8.25 -Goal "(*f* f) xa * (*f* g) xa = (*f* (%x. f x * g x)) xa";
    8.26 +Goal "( *f* f) xa * ( *f* g) xa = ( *f* (%x. f x * g x)) xa";
    8.27  by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
    8.28  by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_mult]));
    8.29  qed "starfun_mult";
    8.30 @@ -218,7 +218,7 @@
    8.31  (*---------------------------------------
    8.32    addition: ( *f ) + ( *g ) = *(f + g)  
    8.33   ---------------------------------------*)
    8.34 -Goal "(*f* f) xa + (*f* g) xa = (*f* (%x. f x + g x)) xa";
    8.35 +Goal "( *f* f) xa + ( *f* g) xa = ( *f* (%x. f x + g x)) xa";
    8.36  by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
    8.37  by (auto_tac (claset(),simpset() addsimps [starfun,hypreal_add]));
    8.38  qed "starfun_add";
    8.39 @@ -228,20 +228,20 @@
    8.40    subtraction: ( *f ) + -( *g ) = *(f + -g)  
    8.41   -------------------------------------------*)
    8.42  
    8.43 -Goal "- (*f* f) x = (*f* (%x. - f x)) x";
    8.44 +Goal "- ( *f* f) x = ( *f* (%x. - f x)) x";
    8.45  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    8.46  by (auto_tac (claset(),simpset() addsimps [starfun, hypreal_minus]));
    8.47  qed "starfun_minus";
    8.48  Addsimps [starfun_minus RS sym];
    8.49  
    8.50  (*FIXME: delete*)
    8.51 -Goal "(*f* f) xa + -(*f* g) xa = (*f* (%x. f x + -g x)) xa";
    8.52 +Goal "( *f* f) xa + -( *f* g) xa = ( *f* (%x. f x + -g x)) xa";
    8.53  by (Simp_tac 1);
    8.54  qed "starfun_add_minus";
    8.55  Addsimps [starfun_add_minus RS sym];
    8.56  
    8.57  Goalw [hypreal_diff_def,real_diff_def]
    8.58 -  "(*f* f) xa  - (*f* g) xa = (*f* (%x. f x - g x)) xa";
    8.59 +  "( *f* f) xa  - ( *f* g) xa = ( *f* (%x. f x - g x)) xa";
    8.60  by (rtac starfun_add_minus 1);
    8.61  qed "starfun_diff";
    8.62  Addsimps [starfun_diff RS sym];
    8.63 @@ -250,20 +250,20 @@
    8.64    composition: ( *f ) o ( *g ) = *(f o g)  
    8.65   ---------------------------------------*)
    8.66  
    8.67 -Goal "(%x. (*f* f) ((*f* g) x)) = *f* (%x. f (g x))"; 
    8.68 +Goal "(%x. ( *f* f) (( *f* g) x)) = *f* (%x. f (g x))"; 
    8.69  by (rtac ext 1);
    8.70  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    8.71  by (auto_tac (claset(),simpset() addsimps [starfun]));
    8.72  qed "starfun_o2";
    8.73  
    8.74 -Goalw [o_def] "(*f* f) o (*f* g) = (*f* (f o g))";
    8.75 +Goalw [o_def] "( *f* f) o ( *f* g) = ( *f* (f o g))";
    8.76  by (simp_tac (simpset() addsimps [starfun_o2]) 1);
    8.77  qed "starfun_o";
    8.78  
    8.79  (*--------------------------------------
    8.80    NS extension of constant function
    8.81   --------------------------------------*)
    8.82 -Goal "(*f* (%x. k)) xa = hypreal_of_real  k";
    8.83 +Goal "( *f* (%x. k)) xa = hypreal_of_real  k";
    8.84  by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
    8.85  by (auto_tac (claset(),simpset() addsimps [starfun,
    8.86      hypreal_of_real_def]));
    8.87 @@ -275,12 +275,12 @@
    8.88     the NS extension of the identity function
    8.89   ----------------------------------------------------*)
    8.90  
    8.91 -Goal "x @= hypreal_of_real a ==> (*f* (%x. x)) x @= hypreal_of_real  a";
    8.92 +Goal "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real  a";
    8.93  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
    8.94  by (auto_tac (claset(),simpset() addsimps [starfun]));
    8.95  qed "starfun_Idfun_approx";
    8.96  
    8.97 -Goal "(*f* (%x. x)) x = x";
    8.98 +Goal "( *f* (%x. x)) x = x";
    8.99  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   8.100  by (auto_tac (claset(),simpset() addsimps [starfun]));
   8.101  qed "starfun_Id";
   8.102 @@ -290,7 +290,7 @@
   8.103        the *-function is a (nonstandard) extension of the function
   8.104   ----------------------------------------------------------------------*)
   8.105  
   8.106 -Goalw [is_starext_def] "is_starext (*f* f) f";
   8.107 +Goalw [is_starext_def] "is_starext ( *f* f) f";
   8.108  by (Auto_tac);
   8.109  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   8.110  by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   8.111 @@ -305,7 +305,7 @@
   8.112  by (rtac ext 1);
   8.113  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   8.114  by (dres_inst_tac [("x","x")] spec 1);
   8.115 -by (dres_inst_tac [("x","(*f* f) x")] spec 1);
   8.116 +by (dres_inst_tac [("x","( *f* f) x")] spec 1);
   8.117  by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
   8.118      simpset() addsimps [starfun]));
   8.119  by (Fuf_empty_tac 1);
   8.120 @@ -320,41 +320,41 @@
   8.121     version for real arguments. i.e they are the same
   8.122     for all real arguments
   8.123   -------------------------------------------------------*)
   8.124 -Goal "(*f* f) (hypreal_of_real a) = hypreal_of_real (f a)";
   8.125 +Goal "( *f* f) (hypreal_of_real a) = hypreal_of_real (f a)";
   8.126  by (auto_tac (claset(),simpset() addsimps 
   8.127       [starfun,hypreal_of_real_def]));
   8.128  qed "starfun_eq";
   8.129  
   8.130  Addsimps [starfun_eq];
   8.131  
   8.132 -Goal "(*f* f) (hypreal_of_real a) @= hypreal_of_real (f a)";
   8.133 +Goal "( *f* f) (hypreal_of_real a) @= hypreal_of_real (f a)";
   8.134  by (Auto_tac);
   8.135  qed "starfun_approx";
   8.136  
   8.137  (* useful for NS definition of derivatives *)
   8.138 -Goal "(*f* (%h. f (x + h))) xa  = (*f* f) (hypreal_of_real  x + xa)";
   8.139 +Goal "( *f* (%h. f (x + h))) xa  = ( *f* f) (hypreal_of_real  x + xa)";
   8.140  by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   8.141  by (auto_tac (claset(),simpset() addsimps [starfun,
   8.142      hypreal_of_real_def,hypreal_add]));
   8.143  qed "starfun_lambda_cancel";
   8.144  
   8.145 -Goal "(*f* (%h. f(g(x + h)))) xa = (*f* (f o g)) (hypreal_of_real x + xa)";
   8.146 +Goal "( *f* (%h. f(g(x + h)))) xa = ( *f* (f o g)) (hypreal_of_real x + xa)";
   8.147  by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
   8.148  by (auto_tac (claset(),simpset() addsimps [starfun,
   8.149      hypreal_of_real_def,hypreal_add]));
   8.150  qed "starfun_lambda_cancel2";
   8.151  
   8.152 -Goal "[| (*f* f) xa @= l; (*f* g) xa @= m; \
   8.153 +Goal "[| ( *f* f) xa @= l; ( *f* g) xa @= m; \
   8.154  \                 l: HFinite; m: HFinite  \
   8.155 -\              |] ==>  (*f* (%x. f x * g x)) xa @= l * m";
   8.156 +\              |] ==>  ( *f* (%x. f x * g x)) xa @= l * m";
   8.157  by (dtac approx_mult_HFinite 1);
   8.158  by (REPEAT(assume_tac 1));
   8.159  by (auto_tac (claset() addIs [approx_sym RSN (2,approx_HFinite)],
   8.160                simpset()));
   8.161  qed "starfun_mult_HFinite_approx";
   8.162  
   8.163 -Goal "[| (*f* f) xa @= l; (*f* g) xa @= m \
   8.164 -\              |] ==>  (*f* (%x. f x + g x)) xa @= l + m";
   8.165 +Goal "[| ( *f* f) xa @= l; ( *f* g) xa @= m \
   8.166 +\              |] ==>  ( *f* (%x. f x + g x)) xa @= l + m";
   8.167  by (auto_tac (claset() addIs [approx_add], simpset()));
   8.168  qed "starfun_add_approx";
   8.169  
   8.170 @@ -372,14 +372,14 @@
   8.171            (is_starext_starfun_iff RS iffD1) RS sym) 1);
   8.172  qed "starfun_rabs_hrabs";
   8.173  
   8.174 -Goal "(*f* inverse) x = inverse(x)";
   8.175 +Goal "( *f* inverse) x = inverse(x)";
   8.176  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   8.177  by (auto_tac (claset(),
   8.178              simpset() addsimps [starfun, hypreal_inverse, hypreal_zero_def]));
   8.179  qed "starfun_inverse_inverse";
   8.180  Addsimps [starfun_inverse_inverse];
   8.181  
   8.182 -Goal "inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
   8.183 +Goal "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x";
   8.184  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   8.185  by (auto_tac (claset(),
   8.186                simpset() addsimps [starfun, hypreal_inverse]));
   8.187 @@ -387,12 +387,12 @@
   8.188  Addsimps [starfun_inverse RS sym];
   8.189  
   8.190  Goalw [hypreal_divide_def,real_divide_def]
   8.191 -  "(*f* f) xa  / (*f* g) xa = (*f* (%x. f x / g x)) xa";
   8.192 +  "( *f* f) xa  / ( *f* g) xa = ( *f* (%x. f x / g x)) xa";
   8.193  by Auto_tac;
   8.194  qed "starfun_divide";
   8.195  Addsimps [starfun_divide RS sym];
   8.196  
   8.197 -Goal "inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
   8.198 +Goal "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x";
   8.199  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   8.200  by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
   8.201                         addSDs [FreeUltrafilterNat_Compl_mem],
   8.202 @@ -404,7 +404,7 @@
   8.203      topology of the reals
   8.204   ------------------------------------------------------------*)
   8.205  Goalw [starset_def] 
   8.206 -      "(*f* f) x : *s* A ==> x : *s* {x. f x : A}";
   8.207 +      "( *f* f) x : *s* A ==> x : *s* {x. f x : A}";
   8.208  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   8.209  by (auto_tac (claset(),simpset() addsimps [starfun]));
   8.210  by (dres_inst_tac [("x","%n. f (Xa n)")] bspec 1);
   8.211 @@ -440,7 +440,7 @@
   8.212  
   8.213  Goalw [starset_def]
   8.214    "*s* {x. abs (f x + - y) < r} = \
   8.215 -\      {x. abs((*f* f) x + -hypreal_of_real y) < hypreal_of_real r}";
   8.216 +\      {x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}";
   8.217  by (Step_tac 1);
   8.218  by (ALLGOALS(res_inst_tac [("z","x")] eq_Abs_hypreal));
   8.219  by (auto_tac (claset() addSIs [exI] addSDs [bspec],