more symbols;
authorwenzelm
Wed Dec 30 18:03:23 2015 +0100 (2015-12-30)
changeset 619823af5a06577c7
parent 61981 1b5845c62fa0
child 61983 8fb53badad99
more symbols;
NEWS
src/HOL/NSA/CStar.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NSA/HLim.thy
src/HOL/NSA/HSeries.thy
src/HOL/NSA/HTranscendental.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/NSCA.thy
src/HOL/NSA/Star.thy
     1.1 --- a/NEWS	Wed Dec 30 17:55:43 2015 +0100
     1.2 +++ b/NEWS	Wed Dec 30 18:03:23 2015 +0100
     1.3 @@ -506,6 +506,7 @@
     1.4    notation (in topological_space) LIMSEQ ("((_)/ ----> (_))" [60, 60] 60)
     1.5    notation LIM ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
     1.6  
     1.7 +  notation NSA.approx (infixl "@=" 50)
     1.8    notation NSLIMSEQ ("((_)/ ----NS> (_))" [60, 60] 60)
     1.9    notation NSLIM ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
    1.10  
     2.1 --- a/src/HOL/NSA/CStar.thy	Wed Dec 30 17:55:43 2015 +0100
     2.2 +++ b/src/HOL/NSA/CStar.thy	Wed Dec 30 18:03:23 2015 +0100
     2.3 @@ -52,8 +52,8 @@
     2.4  by (simp add: hcomplex_hRe_hIm_cancel_iff starfun_Re starfun_Im)
     2.5  
     2.6  lemma starfunC_approx_Re_Im_iff:
     2.7 -    "(( *f* f) x @= z) = ((( *f* (%x. Re(f x))) x @= hRe (z)) &
     2.8 -                            (( *f* (%x. Im(f x))) x @= hIm (z)))"
     2.9 +    "(( *f* f) x \<approx> z) = ((( *f* (%x. Re(f x))) x \<approx> hRe (z)) &
    2.10 +                            (( *f* (%x. Im(f x))) x \<approx> hIm (z)))"
    2.11  by (simp add: hcomplex_approx_iff starfun_Re starfun_Im)
    2.12  
    2.13  end
     3.1 --- a/src/HOL/NSA/HDeriv.thy	Wed Dec 30 17:55:43 2015 +0100
     3.2 +++ b/src/HOL/NSA/HDeriv.thy	Wed Dec 30 18:03:23 2015 +0100
     3.3 @@ -17,7 +17,7 @@
     3.4            ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
     3.5    "NSDERIV f x :> D = (\<forall>h \<in> Infinitesimal - {0}.
     3.6        (( *f* f)(star_of x + h)
     3.7 -       - star_of (f x))/h @= star_of D)"
     3.8 +       - star_of (f x))/h \<approx> star_of D)"
     3.9  
    3.10  definition
    3.11    NSdifferentiable :: "['a::real_normed_field \<Rightarrow> 'a, 'a] \<Rightarrow> bool"
     4.1 --- a/src/HOL/NSA/HLim.thy	Wed Dec 30 17:55:43 2015 +0100
     4.2 +++ b/src/HOL/NSA/HLim.thy	Wed Dec 30 18:03:23 2015 +0100
     4.3 @@ -15,17 +15,17 @@
     4.4    NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
     4.5              ("((_)/ \<midarrow>(_)/\<rightarrow>\<^sub>N\<^sub>S (_))" [60, 0, 60] 60) where
     4.6    "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L =
     4.7 -    (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
     4.8 +    (\<forall>x. (x \<noteq> star_of a & x \<approx> star_of a --> ( *f* f) x \<approx> star_of L))"
     4.9  
    4.10  definition
    4.11    isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
    4.12      \<comment>\<open>NS definition dispenses with limit notions\<close>
    4.13 -  "isNSCont f a = (\<forall>y. y @= star_of a -->
    4.14 -         ( *f* f) y @= star_of (f a))"
    4.15 +  "isNSCont f a = (\<forall>y. y \<approx> star_of a -->
    4.16 +         ( *f* f) y \<approx> star_of (f a))"
    4.17  
    4.18  definition
    4.19    isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
    4.20 -  "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
    4.21 +  "isNSUCont f = (\<forall>x y. x \<approx> y --> ( *f* f) x \<approx> ( *f* f) y)"
    4.22  
    4.23  
    4.24  subsection \<open>Limits of Functions\<close>
     5.1 --- a/src/HOL/NSA/HSeries.thy	Wed Dec 30 17:55:43 2015 +0100
     5.2 +++ b/src/HOL/NSA/HSeries.thy	Wed Dec 30 18:03:23 2015 +0100
     5.3 @@ -129,8 +129,8 @@
     5.4  lemma starfunNat_sumr: "!!N. ( *f* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
     5.5  unfolding sumhr_app by transfer (rule refl)
     5.6  
     5.7 -lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) @= sumhr(0, N, f)
     5.8 -      ==> \<bar>sumhr(M, N, f)\<bar> @= 0"
     5.9 +lemma sumhr_hrabs_approx [simp]: "sumhr(0, M, f) \<approx> sumhr(0, N, f)
    5.10 +      ==> \<bar>sumhr(M, N, f)\<bar> \<approx> 0"
    5.11  apply (cut_tac x = M and y = N in linorder_less_linear)
    5.12  apply (auto simp add: approx_refl)
    5.13  apply (drule approx_sym [THEN approx_minus_iff [THEN iffD1]])
    5.14 @@ -167,7 +167,7 @@
    5.15  
    5.16  lemma NSsummable_NSCauchy:
    5.17       "NSsummable f =
    5.18 -      (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> @= 0)"
    5.19 +      (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. \<bar>sumhr(M,N,f)\<bar> \<approx> 0)"
    5.20  apply (auto simp add: summable_NSsummable_iff [symmetric]
    5.21         summable_iff_convergent convergent_NSconvergent_iff atLeast0LessThan[symmetric]
    5.22         NSCauchy_NSconvergent_iff [symmetric] NSCauchy_def starfunNat_sumr)
     6.1 --- a/src/HOL/NSA/HTranscendental.thy	Wed Dec 30 17:55:43 2015 +0100
     6.2 +++ b/src/HOL/NSA/HTranscendental.thy	Wed Dec 30 18:03:23 2015 +0100
     6.3 @@ -69,7 +69,7 @@
     6.4  by (auto intro: hypreal_sqrt_mult_distrib simp add: order_le_less)
     6.5  
     6.6  lemma hypreal_sqrt_approx_zero [simp]:
     6.7 -     "0 < x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
     6.8 +     "0 < x ==> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
     6.9  apply (auto simp add: mem_infmal_iff [symmetric])
    6.10  apply (rule hypreal_sqrt_gt_zero_pow2 [THEN subst])
    6.11  apply (auto intro: Infinitesimal_mult 
    6.12 @@ -78,18 +78,18 @@
    6.13  done
    6.14  
    6.15  lemma hypreal_sqrt_approx_zero2 [simp]:
    6.16 -     "0 \<le> x ==> (( *f* sqrt)(x) @= 0) = (x @= 0)"
    6.17 +     "0 \<le> x ==> (( *f* sqrt)(x) \<approx> 0) = (x \<approx> 0)"
    6.18  by (auto simp add: order_le_less)
    6.19  
    6.20  lemma hypreal_sqrt_sum_squares [simp]:
    6.21 -     "(( *f* sqrt)(x*x + y*y + z*z) @= 0) = (x*x + y*y + z*z @= 0)"
    6.22 +     "(( *f* sqrt)(x*x + y*y + z*z) \<approx> 0) = (x*x + y*y + z*z \<approx> 0)"
    6.23  apply (rule hypreal_sqrt_approx_zero2)
    6.24  apply (rule add_nonneg_nonneg)+
    6.25  apply (auto)
    6.26  done
    6.27  
    6.28  lemma hypreal_sqrt_sum_squares2 [simp]:
    6.29 -     "(( *f* sqrt)(x*x + y*y) @= 0) = (x*x + y*y @= 0)"
    6.30 +     "(( *f* sqrt)(x*x + y*y) \<approx> 0) = (x*x + y*y \<approx> 0)"
    6.31  apply (rule hypreal_sqrt_approx_zero2)
    6.32  apply (rule add_nonneg_nonneg)
    6.33  apply (auto)
    6.34 @@ -242,12 +242,12 @@
    6.35  apply (unfold sumhr_app, transfer, simp add: cos_coeff_def power_0_left)
    6.36  done
    6.37  
    6.38 -lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) @= 1"
    6.39 +lemma STAR_exp_zero_approx_one [simp]: "( *f* exp) (0::hypreal) \<approx> 1"
    6.40  apply (subgoal_tac "( *f* exp) (0::hypreal) = 1", simp)
    6.41  apply (transfer, simp)
    6.42  done
    6.43  
    6.44 -lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) (x::hypreal) @= 1"
    6.45 +lemma STAR_exp_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* exp) (x::hypreal) \<approx> 1"
    6.46  apply (case_tac "x = 0")
    6.47  apply (cut_tac [2] x = 0 in DERIV_exp)
    6.48  apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
    6.49 @@ -260,7 +260,7 @@
    6.50  apply (auto simp add: mem_infmal_iff)
    6.51  done
    6.52  
    6.53 -lemma STAR_exp_epsilon [simp]: "( *f* exp) \<epsilon> @= 1"
    6.54 +lemma STAR_exp_epsilon [simp]: "( *f* exp) \<epsilon> \<approx> 1"
    6.55  by (auto intro: STAR_exp_Infinitesimal)
    6.56  
    6.57  lemma STAR_exp_add:
    6.58 @@ -354,7 +354,7 @@
    6.59  done
    6.60  
    6.61  lemma starfun_exp_add_HFinite_Infinitesimal_approx:
    6.62 -     "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x::hypreal) @= ( *f* exp) z"
    6.63 +     "[|x \<in> Infinitesimal; z \<in> HFinite |] ==> ( *f* exp) (z + x::hypreal) \<approx> ( *f* exp) z"
    6.64  apply (simp add: STAR_exp_add)
    6.65  apply (frule STAR_exp_Infinitesimal)
    6.66  apply (drule approx_mult2)
    6.67 @@ -425,7 +425,7 @@
    6.68  
    6.69  lemma STAR_sin_Infinitesimal [simp]:
    6.70    fixes x :: "'a::{real_normed_field,banach} star"
    6.71 -  shows "x \<in> Infinitesimal ==> ( *f* sin) x @= x"
    6.72 +  shows "x \<in> Infinitesimal ==> ( *f* sin) x \<approx> x"
    6.73  apply (case_tac "x = 0")
    6.74  apply (cut_tac [2] x = 0 in DERIV_sin)
    6.75  apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
    6.76 @@ -451,7 +451,7 @@
    6.77  
    6.78  lemma STAR_cos_Infinitesimal [simp]:
    6.79    fixes x :: "'a::{real_normed_field,banach} star"
    6.80 -  shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 1"
    6.81 +  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1"
    6.82  apply (case_tac "x = 0")
    6.83  apply (cut_tac [2] x = 0 in DERIV_cos)
    6.84  apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
    6.85 @@ -467,7 +467,7 @@
    6.86  lemma STAR_tan_zero [simp]: "( *f* tan) 0 = 0"
    6.87  by transfer (rule tan_zero)
    6.88  
    6.89 -lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x @= x"
    6.90 +lemma STAR_tan_Infinitesimal: "x \<in> Infinitesimal ==> ( *f* tan) x \<approx> x"
    6.91  apply (case_tac "x = 0")
    6.92  apply (cut_tac [2] x = 0 in DERIV_tan)
    6.93  apply (auto simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
    6.94 @@ -479,7 +479,7 @@
    6.95  
    6.96  lemma STAR_sin_cos_Infinitesimal_mult:
    6.97    fixes x :: "'a::{real_normed_field,banach} star"
    6.98 -  shows "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x @= x"
    6.99 +  shows "x \<in> Infinitesimal ==> ( *f* sin) x * ( *f* cos) x \<approx> x"
   6.100  using approx_mult_HFinite [of "( *f* sin) x" _ "( *f* cos) x" 1] 
   6.101  by (simp add: Infinitesimal_subset_HFinite [THEN subsetD])
   6.102  
   6.103 @@ -496,24 +496,24 @@
   6.104  
   6.105  lemma STAR_sin_Infinitesimal_divide:
   6.106    fixes x :: "'a::{real_normed_field,banach} star"
   6.107 -  shows "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x @= 1"
   6.108 +  shows "[|x \<in> Infinitesimal; x \<noteq> 0 |] ==> ( *f* sin) x/x \<approx> 1"
   6.109  using DERIV_sin [of "0::'a"]
   6.110  by (simp add: NSDERIV_DERIV_iff [symmetric] nsderiv_def)
   6.111  
   6.112  (*------------------------------------------------------------------------*) 
   6.113 -(* sin* (1/n) * 1/(1/n) @= 1 for n = oo                                   *)
   6.114 +(* sin* (1/n) * 1/(1/n) \<approx> 1 for n = oo                                   *)
   6.115  (*------------------------------------------------------------------------*)
   6.116  
   6.117  lemma lemma_sin_pi:
   6.118       "n \<in> HNatInfinite  
   6.119 -      ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1"
   6.120 +      ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) \<approx> 1"
   6.121  apply (rule STAR_sin_Infinitesimal_divide)
   6.122  apply (auto simp add: zero_less_HNatInfinite)
   6.123  done
   6.124  
   6.125  lemma STAR_sin_inverse_HNatInfinite:
   6.126       "n \<in> HNatInfinite  
   6.127 -      ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n @= 1"
   6.128 +      ==> ( *f* sin) (inverse (hypreal_of_hypnat n)) * hypreal_of_hypnat n \<approx> 1"
   6.129  apply (frule lemma_sin_pi)
   6.130  apply (simp add: divide_inverse)
   6.131  done
   6.132 @@ -532,7 +532,7 @@
   6.133  lemma STAR_sin_pi_divide_HNatInfinite_approx_pi:
   6.134       "n \<in> HNatInfinite  
   6.135        ==> ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n)) * hypreal_of_hypnat n  
   6.136 -          @= hypreal_of_real pi"
   6.137 +          \<approx> hypreal_of_real pi"
   6.138  apply (frule STAR_sin_Infinitesimal_divide
   6.139                 [OF Infinitesimal_pi_divide_HNatInfinite 
   6.140                     pi_divide_HNatInfinite_not_zero])
   6.141 @@ -545,7 +545,7 @@
   6.142       "n \<in> HNatInfinite  
   6.143        ==> hypreal_of_hypnat n *  
   6.144            ( *f* sin) (hypreal_of_real pi/(hypreal_of_hypnat n))  
   6.145 -          @= hypreal_of_real pi"
   6.146 +          \<approx> hypreal_of_real pi"
   6.147  apply (rule mult.commute [THEN subst])
   6.148  apply (erule STAR_sin_pi_divide_HNatInfinite_approx_pi)
   6.149  done
   6.150 @@ -558,7 +558,7 @@
   6.151  
   6.152  lemma STAR_sin_pi_divide_n_approx:
   6.153       "N \<in> HNatInfinite ==>  
   6.154 -      ( *f* sin) (( *f* (%x. pi / real x)) N) @=  
   6.155 +      ( *f* sin) (( *f* (%x. pi / real x)) N) \<approx>  
   6.156        hypreal_of_real pi/(hypreal_of_hypnat N)"
   6.157  apply (simp add: starfunNat_real_of_nat [symmetric])
   6.158  apply (rule STAR_sin_Infinitesimal)
   6.159 @@ -596,7 +596,7 @@
   6.160  
   6.161  lemma STAR_cos_Infinitesimal_approx:
   6.162    fixes x :: "'a::{real_normed_field,banach} star"
   6.163 -  shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - x\<^sup>2"
   6.164 +  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - x\<^sup>2"
   6.165  apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   6.166  apply (auto simp add: Infinitesimal_approx_minus [symmetric] 
   6.167              add.assoc [symmetric] numeral_2_eq_2)
   6.168 @@ -604,7 +604,7 @@
   6.169  
   6.170  lemma STAR_cos_Infinitesimal_approx2:
   6.171    fixes x :: hypreal  \<comment>\<open>perhaps could be generalised, like many other hypreal results\<close>
   6.172 -  shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x\<^sup>2)/2"
   6.173 +  shows "x \<in> Infinitesimal ==> ( *f* cos) x \<approx> 1 - (x\<^sup>2)/2"
   6.174  apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   6.175  apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult
   6.176              simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
     7.1 --- a/src/HOL/NSA/NSA.thy	Wed Dec 30 17:55:43 2015 +0100
     7.2 +++ b/src/HOL/NSA/NSA.thy	Wed Dec 30 18:03:23 2015 +0100
     7.3 @@ -26,26 +26,23 @@
     7.4    "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
     7.5  
     7.6  definition
     7.7 -  approx :: "['a::real_normed_vector star, 'a star] => bool"  (infixl "@=" 50) where
     7.8 +  approx :: "['a::real_normed_vector star, 'a star] => bool"  (infixl "\<approx>" 50) where
     7.9      \<comment>\<open>the `infinitely close' relation\<close>
    7.10 -  "(x @= y) = ((x - y) \<in> Infinitesimal)"
    7.11 +  "(x \<approx> y) = ((x - y) \<in> Infinitesimal)"
    7.12  
    7.13  definition
    7.14    st        :: "hypreal => hypreal" where
    7.15      \<comment>\<open>the standard part of a hyperreal\<close>
    7.16 -  "st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r @= x)"
    7.17 +  "st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r \<approx> x)"
    7.18  
    7.19  definition
    7.20    monad     :: "'a::real_normed_vector star => 'a star set" where
    7.21 -  "monad x = {y. x @= y}"
    7.22 +  "monad x = {y. x \<approx> y}"
    7.23  
    7.24  definition
    7.25    galaxy    :: "'a::real_normed_vector star => 'a star set" where
    7.26    "galaxy x = {y. (x + -y) \<in> HFinite}"
    7.27  
    7.28 -notation (xsymbols)
    7.29 -  approx  (infixl "\<approx>" 50)
    7.30 -
    7.31  lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}"
    7.32  by (simp add: Reals_def image_def)
    7.33  
    7.34 @@ -611,46 +608,46 @@
    7.35  
    7.36  subsection\<open>The Infinitely Close Relation\<close>
    7.37  
    7.38 -lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)"
    7.39 +lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x \<approx> 0)"
    7.40  by (simp add: Infinitesimal_def approx_def)
    7.41  
    7.42 -lemma approx_minus_iff: " (x @= y) = (x - y @= 0)"
    7.43 +lemma approx_minus_iff: " (x \<approx> y) = (x - y \<approx> 0)"
    7.44  by (simp add: approx_def)
    7.45  
    7.46 -lemma approx_minus_iff2: " (x @= y) = (-y + x @= 0)"
    7.47 +lemma approx_minus_iff2: " (x \<approx> y) = (-y + x \<approx> 0)"
    7.48  by (simp add: approx_def add.commute)
    7.49  
    7.50 -lemma approx_refl [iff]: "x @= x"
    7.51 +lemma approx_refl [iff]: "x \<approx> x"
    7.52  by (simp add: approx_def Infinitesimal_def)
    7.53  
    7.54  lemma hypreal_minus_distrib1: "-(y + -(x::'a::ab_group_add)) = x + -y"
    7.55  by (simp add: add.commute)
    7.56  
    7.57 -lemma approx_sym: "x @= y ==> y @= x"
    7.58 +lemma approx_sym: "x \<approx> y ==> y \<approx> x"
    7.59  apply (simp add: approx_def)
    7.60  apply (drule Infinitesimal_minus_iff [THEN iffD2])
    7.61  apply simp
    7.62  done
    7.63  
    7.64 -lemma approx_trans: "[| x @= y; y @= z |] ==> x @= z"
    7.65 +lemma approx_trans: "[| x \<approx> y; y \<approx> z |] ==> x \<approx> z"
    7.66  apply (simp add: approx_def)
    7.67  apply (drule (1) Infinitesimal_add)
    7.68  apply simp
    7.69  done
    7.70  
    7.71 -lemma approx_trans2: "[| r @= x; s @= x |] ==> r @= s"
    7.72 +lemma approx_trans2: "[| r \<approx> x; s \<approx> x |] ==> r \<approx> s"
    7.73  by (blast intro: approx_sym approx_trans)
    7.74  
    7.75 -lemma approx_trans3: "[| x @= r; x @= s|] ==> r @= s"
    7.76 +lemma approx_trans3: "[| x \<approx> r; x \<approx> s|] ==> r \<approx> s"
    7.77  by (blast intro: approx_sym approx_trans)
    7.78  
    7.79 -lemma approx_reorient: "(x @= y) = (y @= x)"
    7.80 +lemma approx_reorient: "(x \<approx> y) = (y \<approx> x)"
    7.81  by (blast intro: approx_sym)
    7.82  
    7.83  (*reorientation simplification procedure: reorients (polymorphic)
    7.84    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
    7.85  simproc_setup approx_reorient_simproc
    7.86 -  ("0 @= x" | "1 @= y" | "numeral w @= z" | "- 1 @= y" | "- numeral w @= r") =
    7.87 +  ("0 \<approx> x" | "1 \<approx> y" | "numeral w \<approx> z" | "- 1 \<approx> y" | "- numeral w \<approx> r") =
    7.88  \<open>
    7.89    let val rule = @{thm approx_reorient} RS eq_reflection
    7.90        fun proc phi ss ct =
    7.91 @@ -661,21 +658,21 @@
    7.92    in proc end
    7.93  \<close>
    7.94  
    7.95 -lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"
    7.96 +lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x \<approx> y)"
    7.97  by (simp add: approx_minus_iff [symmetric] mem_infmal_iff)
    7.98  
    7.99 -lemma approx_monad_iff: "(x @= y) = (monad(x)=monad(y))"
   7.100 +lemma approx_monad_iff: "(x \<approx> y) = (monad(x)=monad(y))"
   7.101  apply (simp add: monad_def)
   7.102  apply (auto dest: approx_sym elim!: approx_trans equalityCE)
   7.103  done
   7.104  
   7.105  lemma Infinitesimal_approx:
   7.106 -     "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x @= y"
   7.107 +     "[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> x \<approx> y"
   7.108  apply (simp add: mem_infmal_iff)
   7.109  apply (blast intro: approx_trans approx_sym)
   7.110  done
   7.111  
   7.112 -lemma approx_add: "[| a @= b; c @= d |] ==> a+c @= b+d"
   7.113 +lemma approx_add: "[| a \<approx> b; c \<approx> d |] ==> a+c \<approx> b+d"
   7.114  proof (unfold approx_def)
   7.115    assume inf: "a - b \<in> Infinitesimal" "c - d \<in> Infinitesimal"
   7.116    have "a + c - (b + d) = (a - b) + (c - d)" by simp
   7.117 @@ -683,132 +680,132 @@
   7.118    finally show "a + c - (b + d) \<in> Infinitesimal" .
   7.119  qed
   7.120  
   7.121 -lemma approx_minus: "a @= b ==> -a @= -b"
   7.122 +lemma approx_minus: "a \<approx> b ==> -a \<approx> -b"
   7.123  apply (rule approx_minus_iff [THEN iffD2, THEN approx_sym])
   7.124  apply (drule approx_minus_iff [THEN iffD1])
   7.125  apply (simp add: add.commute)
   7.126  done
   7.127  
   7.128 -lemma approx_minus2: "-a @= -b ==> a @= b"
   7.129 +lemma approx_minus2: "-a \<approx> -b ==> a \<approx> b"
   7.130  by (auto dest: approx_minus)
   7.131  
   7.132 -lemma approx_minus_cancel [simp]: "(-a @= -b) = (a @= b)"
   7.133 +lemma approx_minus_cancel [simp]: "(-a \<approx> -b) = (a \<approx> b)"
   7.134  by (blast intro: approx_minus approx_minus2)
   7.135  
   7.136 -lemma approx_add_minus: "[| a @= b; c @= d |] ==> a + -c @= b + -d"
   7.137 +lemma approx_add_minus: "[| a \<approx> b; c \<approx> d |] ==> a + -c \<approx> b + -d"
   7.138  by (blast intro!: approx_add approx_minus)
   7.139  
   7.140 -lemma approx_diff: "[| a @= b; c @= d |] ==> a - c @= b - d"
   7.141 +lemma approx_diff: "[| a \<approx> b; c \<approx> d |] ==> a - c \<approx> b - d"
   7.142    using approx_add [of a b "- c" "- d"] by simp
   7.143  
   7.144  lemma approx_mult1:
   7.145    fixes a b c :: "'a::real_normed_algebra star"
   7.146 -  shows "[| a @= b; c: HFinite|] ==> a*c @= b*c"
   7.147 +  shows "[| a \<approx> b; c: HFinite|] ==> a*c \<approx> b*c"
   7.148  by (simp add: approx_def Infinitesimal_HFinite_mult
   7.149                left_diff_distrib [symmetric])
   7.150  
   7.151  lemma approx_mult2:
   7.152    fixes a b c :: "'a::real_normed_algebra star"
   7.153 -  shows "[|a @= b; c: HFinite|] ==> c*a @= c*b"
   7.154 +  shows "[|a \<approx> b; c: HFinite|] ==> c*a \<approx> c*b"
   7.155  by (simp add: approx_def Infinitesimal_HFinite_mult2
   7.156                right_diff_distrib [symmetric])
   7.157  
   7.158  lemma approx_mult_subst:
   7.159    fixes u v x y :: "'a::real_normed_algebra star"
   7.160 -  shows "[|u @= v*x; x @= y; v \<in> HFinite|] ==> u @= v*y"
   7.161 +  shows "[|u \<approx> v*x; x \<approx> y; v \<in> HFinite|] ==> u \<approx> v*y"
   7.162  by (blast intro: approx_mult2 approx_trans)
   7.163  
   7.164  lemma approx_mult_subst2:
   7.165    fixes u v x y :: "'a::real_normed_algebra star"
   7.166 -  shows "[| u @= x*v; x @= y; v \<in> HFinite |] ==> u @= y*v"
   7.167 +  shows "[| u \<approx> x*v; x \<approx> y; v \<in> HFinite |] ==> u \<approx> y*v"
   7.168  by (blast intro: approx_mult1 approx_trans)
   7.169  
   7.170  lemma approx_mult_subst_star_of:
   7.171    fixes u x y :: "'a::real_normed_algebra star"
   7.172 -  shows "[| u @= x*star_of v; x @= y |] ==> u @= y*star_of v"
   7.173 +  shows "[| u \<approx> x*star_of v; x \<approx> y |] ==> u \<approx> y*star_of v"
   7.174  by (auto intro: approx_mult_subst2)
   7.175  
   7.176 -lemma approx_eq_imp: "a = b ==> a @= b"
   7.177 +lemma approx_eq_imp: "a = b ==> a \<approx> b"
   7.178  by (simp add: approx_def)
   7.179  
   7.180 -lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x @= x"
   7.181 +lemma Infinitesimal_minus_approx: "x \<in> Infinitesimal ==> -x \<approx> x"
   7.182  by (blast intro: Infinitesimal_minus_iff [THEN iffD2]
   7.183                      mem_infmal_iff [THEN iffD1] approx_trans2)
   7.184  
   7.185 -lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x - z = y) = (x @= z)"
   7.186 +lemma bex_Infinitesimal_iff: "(\<exists>y \<in> Infinitesimal. x - z = y) = (x \<approx> z)"
   7.187  by (simp add: approx_def)
   7.188  
   7.189 -lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x @= z)"
   7.190 +lemma bex_Infinitesimal_iff2: "(\<exists>y \<in> Infinitesimal. x = z + y) = (x \<approx> z)"
   7.191  by (force simp add: bex_Infinitesimal_iff [symmetric])
   7.192  
   7.193 -lemma Infinitesimal_add_approx: "[| y \<in> Infinitesimal; x + y = z |] ==> x @= z"
   7.194 +lemma Infinitesimal_add_approx: "[| y \<in> Infinitesimal; x + y = z |] ==> x \<approx> z"
   7.195  apply (rule bex_Infinitesimal_iff [THEN iffD1])
   7.196  apply (drule Infinitesimal_minus_iff [THEN iffD2])
   7.197  apply (auto simp add: add.assoc [symmetric])
   7.198  done
   7.199  
   7.200 -lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x @= x + y"
   7.201 +lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x \<approx> x + y"
   7.202  apply (rule bex_Infinitesimal_iff [THEN iffD1])
   7.203  apply (drule Infinitesimal_minus_iff [THEN iffD2])
   7.204  apply (auto simp add: add.assoc [symmetric])
   7.205  done
   7.206  
   7.207 -lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x @= y + x"
   7.208 +lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x \<approx> y + x"
   7.209  by (auto dest: Infinitesimal_add_approx_self simp add: add.commute)
   7.210  
   7.211 -lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x @= x + -y"
   7.212 +lemma Infinitesimal_add_minus_approx_self: "y \<in> Infinitesimal ==> x \<approx> x + -y"
   7.213  by (blast intro!: Infinitesimal_add_approx_self Infinitesimal_minus_iff [THEN iffD2])
   7.214  
   7.215 -lemma Infinitesimal_add_cancel: "[| y \<in> Infinitesimal; x+y @= z|] ==> x @= z"
   7.216 +lemma Infinitesimal_add_cancel: "[| y \<in> Infinitesimal; x+y \<approx> z|] ==> x \<approx> z"
   7.217  apply (drule_tac x = x in Infinitesimal_add_approx_self [THEN approx_sym])
   7.218  apply (erule approx_trans3 [THEN approx_sym], assumption)
   7.219  done
   7.220  
   7.221  lemma Infinitesimal_add_right_cancel:
   7.222 -     "[| y \<in> Infinitesimal; x @= z + y|] ==> x @= z"
   7.223 +     "[| y \<in> Infinitesimal; x \<approx> z + y|] ==> x \<approx> z"
   7.224  apply (drule_tac x = z in Infinitesimal_add_approx_self2 [THEN approx_sym])
   7.225  apply (erule approx_trans3 [THEN approx_sym])
   7.226  apply (simp add: add.commute)
   7.227  apply (erule approx_sym)
   7.228  done
   7.229  
   7.230 -lemma approx_add_left_cancel: "d + b  @= d + c ==> b @= c"
   7.231 +lemma approx_add_left_cancel: "d + b  \<approx> d + c ==> b \<approx> c"
   7.232  apply (drule approx_minus_iff [THEN iffD1])
   7.233  apply (simp add: approx_minus_iff [symmetric] ac_simps)
   7.234  done
   7.235  
   7.236 -lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c"
   7.237 +lemma approx_add_right_cancel: "b + d \<approx> c + d ==> b \<approx> c"
   7.238  apply (rule approx_add_left_cancel)
   7.239  apply (simp add: add.commute)
   7.240  done
   7.241  
   7.242 -lemma approx_add_mono1: "b @= c ==> d + b @= d + c"
   7.243 +lemma approx_add_mono1: "b \<approx> c ==> d + b \<approx> d + c"
   7.244  apply (rule approx_minus_iff [THEN iffD2])
   7.245  apply (simp add: approx_minus_iff [symmetric] ac_simps)
   7.246  done
   7.247  
   7.248 -lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
   7.249 +lemma approx_add_mono2: "b \<approx> c ==> b + a \<approx> c + a"
   7.250  by (simp add: add.commute approx_add_mono1)
   7.251  
   7.252 -lemma approx_add_left_iff [simp]: "(a + b @= a + c) = (b @= c)"
   7.253 +lemma approx_add_left_iff [simp]: "(a + b \<approx> a + c) = (b \<approx> c)"
   7.254  by (fast elim: approx_add_left_cancel approx_add_mono1)
   7.255  
   7.256 -lemma approx_add_right_iff [simp]: "(b + a @= c + a) = (b @= c)"
   7.257 +lemma approx_add_right_iff [simp]: "(b + a \<approx> c + a) = (b \<approx> c)"
   7.258  by (simp add: add.commute)
   7.259  
   7.260 -lemma approx_HFinite: "[| x \<in> HFinite; x @= y |] ==> y \<in> HFinite"
   7.261 +lemma approx_HFinite: "[| x \<in> HFinite; x \<approx> y |] ==> y \<in> HFinite"
   7.262  apply (drule bex_Infinitesimal_iff2 [THEN iffD2], safe)
   7.263  apply (drule Infinitesimal_subset_HFinite [THEN subsetD, THEN HFinite_minus_iff [THEN iffD2]])
   7.264  apply (drule HFinite_add)
   7.265  apply (auto simp add: add.assoc)
   7.266  done
   7.267  
   7.268 -lemma approx_star_of_HFinite: "x @= star_of D ==> x \<in> HFinite"
   7.269 +lemma approx_star_of_HFinite: "x \<approx> star_of D ==> x \<in> HFinite"
   7.270  by (rule approx_sym [THEN [2] approx_HFinite], auto)
   7.271  
   7.272  lemma approx_mult_HFinite:
   7.273    fixes a b c d :: "'a::real_normed_algebra star"
   7.274 -  shows "[|a @= b; c @= d; b: HFinite; d: HFinite|] ==> a*c @= b*d"
   7.275 +  shows "[|a \<approx> b; c \<approx> d; b: HFinite; d: HFinite|] ==> a*c \<approx> b*d"
   7.276  apply (rule approx_trans)
   7.277  apply (rule_tac [2] approx_mult2)
   7.278  apply (rule approx_mult1)
   7.279 @@ -820,7 +817,7 @@
   7.280  by transfer (rule scaleR_left_diff_distrib)
   7.281  
   7.282  lemma approx_scaleR1:
   7.283 -  "[| a @= star_of b; c: HFinite|] ==> scaleHR a c @= b *\<^sub>R c"
   7.284 +  "[| a \<approx> star_of b; c: HFinite|] ==> scaleHR a c \<approx> b *\<^sub>R c"
   7.285  apply (unfold approx_def)
   7.286  apply (drule (1) Infinitesimal_HFinite_scaleHR)
   7.287  apply (simp only: scaleHR_left_diff_distrib)
   7.288 @@ -828,12 +825,12 @@
   7.289  done
   7.290  
   7.291  lemma approx_scaleR2:
   7.292 -  "a @= b ==> c *\<^sub>R a @= c *\<^sub>R b"
   7.293 +  "a \<approx> b ==> c *\<^sub>R a \<approx> c *\<^sub>R b"
   7.294  by (simp add: approx_def Infinitesimal_scaleR2
   7.295                scaleR_right_diff_distrib [symmetric])
   7.296  
   7.297  lemma approx_scaleR_HFinite:
   7.298 -  "[|a @= star_of b; c @= d; d: HFinite|] ==> scaleHR a c @= b *\<^sub>R d"
   7.299 +  "[|a \<approx> star_of b; c \<approx> d; d: HFinite|] ==> scaleHR a c \<approx> b *\<^sub>R d"
   7.300  apply (rule approx_trans)
   7.301  apply (rule_tac [2] approx_scaleR2)
   7.302  apply (rule approx_scaleR1)
   7.303 @@ -842,38 +839,38 @@
   7.304  
   7.305  lemma approx_mult_star_of:
   7.306    fixes a c :: "'a::real_normed_algebra star"
   7.307 -  shows "[|a @= star_of b; c @= star_of d |]
   7.308 -      ==> a*c @= star_of b*star_of d"
   7.309 +  shows "[|a \<approx> star_of b; c \<approx> star_of d |]
   7.310 +      ==> a*c \<approx> star_of b*star_of d"
   7.311  by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
   7.312  
   7.313  lemma approx_SReal_mult_cancel_zero:
   7.314 -     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
   7.315 +     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a*x \<approx> 0 |] ==> x \<approx> 0"
   7.316  apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   7.317  apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   7.318  done
   7.319  
   7.320 -lemma approx_mult_SReal1: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> x*a @= 0"
   7.321 +lemma approx_mult_SReal1: "[| (a::hypreal) \<in> \<real>; x \<approx> 0 |] ==> x*a \<approx> 0"
   7.322  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
   7.323  
   7.324 -lemma approx_mult_SReal2: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> a*x @= 0"
   7.325 +lemma approx_mult_SReal2: "[| (a::hypreal) \<in> \<real>; x \<approx> 0 |] ==> a*x \<approx> 0"
   7.326  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
   7.327  
   7.328  lemma approx_mult_SReal_zero_cancel_iff [simp]:
   7.329 -     "[|(a::hypreal) \<in> \<real>; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
   7.330 +     "[|(a::hypreal) \<in> \<real>; a \<noteq> 0 |] ==> (a*x \<approx> 0) = (x \<approx> 0)"
   7.331  by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
   7.332  
   7.333  lemma approx_SReal_mult_cancel:
   7.334 -     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
   7.335 +     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a* w \<approx> a*z |] ==> w \<approx> z"
   7.336  apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   7.337  apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   7.338  done
   7.339  
   7.340  lemma approx_SReal_mult_cancel_iff1 [simp]:
   7.341 -     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
   7.342 +     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0|] ==> (a* w \<approx> a*z) = (w \<approx> z)"
   7.343  by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
   7.344           intro: approx_SReal_mult_cancel)
   7.345  
   7.346 -lemma approx_le_bound: "[| (z::hypreal) \<le> f; f @= g; g \<le> z |] ==> f @= z"
   7.347 +lemma approx_le_bound: "[| (z::hypreal) \<le> f; f \<approx> g; g \<le> z |] ==> f \<approx> z"
   7.348  apply (simp add: bex_Infinitesimal_iff2 [symmetric], auto)
   7.349  apply (rule_tac x = "g+y-z" in bexI)
   7.350  apply (simp (no_asm))
   7.351 @@ -968,13 +965,13 @@
   7.352  done
   7.353  
   7.354  lemma approx_SReal_not_zero:
   7.355 -  "[| (y::hypreal) \<in> \<real>; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
   7.356 +  "[| (y::hypreal) \<in> \<real>; x \<approx> y; y\<noteq> 0 |] ==> x \<noteq> 0"
   7.357  apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
   7.358  apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
   7.359  done
   7.360  
   7.361  lemma HFinite_diff_Infinitesimal_approx:
   7.362 -     "[| x @= y; y \<in> HFinite - Infinitesimal |]
   7.363 +     "[| x \<approx> y; y \<in> HFinite - Infinitesimal |]
   7.364        ==> x \<in> HFinite - Infinitesimal"
   7.365  apply (auto intro: approx_sym [THEN [2] approx_HFinite]
   7.366              simp add: mem_infmal_iff)
   7.367 @@ -1006,7 +1003,7 @@
   7.368  
   7.369  subsection\<open>Uniqueness: Two Infinitely Close Reals are Equal\<close>
   7.370  
   7.371 -lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"
   7.372 +lemma star_of_approx_iff [simp]: "(star_of x \<approx> star_of y) = (x = y)"
   7.373  apply safe
   7.374  apply (simp add: approx_def)
   7.375  apply (simp only: star_of_diff [symmetric])
   7.376 @@ -1015,7 +1012,7 @@
   7.377  done
   7.378  
   7.379  lemma SReal_approx_iff:
   7.380 -  "[|(x::hypreal) \<in> \<real>; y \<in> \<real>|] ==> (x @= y) = (x = y)"
   7.381 +  "[|(x::hypreal) \<in> \<real>; y \<in> \<real>|] ==> (x \<approx> y) = (x = y)"
   7.382  apply auto
   7.383  apply (simp add: approx_def)
   7.384  apply (drule (1) Reals_diff)
   7.385 @@ -1024,40 +1021,40 @@
   7.386  done
   7.387  
   7.388  lemma numeral_approx_iff [simp]:
   7.389 -     "(numeral v @= (numeral w :: 'a::{numeral,real_normed_vector} star)) =
   7.390 +     "(numeral v \<approx> (numeral w :: 'a::{numeral,real_normed_vector} star)) =
   7.391        (numeral v = (numeral w :: 'a))"
   7.392  apply (unfold star_numeral_def)
   7.393  apply (rule star_of_approx_iff)
   7.394  done
   7.395  
   7.396 -(*And also for 0 @= #nn and 1 @= #nn, #nn @= 0 and #nn @= 1.*)
   7.397 +(*And also for 0 \<approx> #nn and 1 \<approx> #nn, #nn \<approx> 0 and #nn \<approx> 1.*)
   7.398  lemma [simp]:
   7.399 -  "(numeral w @= (0::'a::{numeral,real_normed_vector} star)) =
   7.400 +  "(numeral w \<approx> (0::'a::{numeral,real_normed_vector} star)) =
   7.401     (numeral w = (0::'a))"
   7.402 -  "((0::'a::{numeral,real_normed_vector} star) @= numeral w) =
   7.403 +  "((0::'a::{numeral,real_normed_vector} star) \<approx> numeral w) =
   7.404     (numeral w = (0::'a))"
   7.405 -  "(numeral w @= (1::'b::{numeral,one,real_normed_vector} star)) =
   7.406 +  "(numeral w \<approx> (1::'b::{numeral,one,real_normed_vector} star)) =
   7.407     (numeral w = (1::'b))"
   7.408 -  "((1::'b::{numeral,one,real_normed_vector} star) @= numeral w) =
   7.409 +  "((1::'b::{numeral,one,real_normed_vector} star) \<approx> numeral w) =
   7.410     (numeral w = (1::'b))"
   7.411 -  "~ (0 @= (1::'c::{zero_neq_one,real_normed_vector} star))"
   7.412 -  "~ (1 @= (0::'c::{zero_neq_one,real_normed_vector} star))"
   7.413 +  "~ (0 \<approx> (1::'c::{zero_neq_one,real_normed_vector} star))"
   7.414 +  "~ (1 \<approx> (0::'c::{zero_neq_one,real_normed_vector} star))"
   7.415  apply (unfold star_numeral_def star_zero_def star_one_def)
   7.416  apply (unfold star_of_approx_iff)
   7.417  by (auto intro: sym)
   7.418  
   7.419  lemma star_of_approx_numeral_iff [simp]:
   7.420 -     "(star_of k @= numeral w) = (k = numeral w)"
   7.421 +     "(star_of k \<approx> numeral w) = (k = numeral w)"
   7.422  by (subst star_of_approx_iff [symmetric], auto)
   7.423  
   7.424 -lemma star_of_approx_zero_iff [simp]: "(star_of k @= 0) = (k = 0)"
   7.425 +lemma star_of_approx_zero_iff [simp]: "(star_of k \<approx> 0) = (k = 0)"
   7.426  by (simp_all add: star_of_approx_iff [symmetric])
   7.427  
   7.428 -lemma star_of_approx_one_iff [simp]: "(star_of k @= 1) = (k = 1)"
   7.429 +lemma star_of_approx_one_iff [simp]: "(star_of k \<approx> 1) = (k = 1)"
   7.430  by (simp_all add: star_of_approx_iff [symmetric])
   7.431  
   7.432  lemma approx_unique_real:
   7.433 -     "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r @= x; s @= x|] ==> r = s"
   7.434 +     "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r \<approx> x; s \<approx> x|] ==> r = s"
   7.435  by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
   7.436  
   7.437  
   7.438 @@ -1265,13 +1262,13 @@
   7.439  done
   7.440  
   7.441  lemma st_part_Ex:
   7.442 -     "(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x @= t"
   7.443 +     "(x::hypreal) \<in> HFinite ==> \<exists>t \<in> Reals. x \<approx> t"
   7.444  apply (simp add: approx_def Infinitesimal_def)
   7.445  apply (drule lemma_st_part_Ex, auto)
   7.446  done
   7.447  
   7.448  text\<open>There is a unique real infinitely close\<close>
   7.449 -lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x @= t"
   7.450 +lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x \<approx> t"
   7.451  apply (drule st_part_Ex, safe)
   7.452  apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
   7.453  apply (auto intro!: approx_unique_real)
   7.454 @@ -1345,8 +1342,8 @@
   7.455  lemma approx_inverse:
   7.456    fixes x y :: "'a::real_normed_div_algebra star"
   7.457    shows
   7.458 -     "[| x @= y; y \<in>  HFinite - Infinitesimal |]
   7.459 -      ==> inverse x @= inverse y"
   7.460 +     "[| x \<approx> y; y \<in>  HFinite - Infinitesimal |]
   7.461 +      ==> inverse x \<approx> inverse y"
   7.462  apply (frule HFinite_diff_Infinitesimal_approx, assumption)
   7.463  apply (frule not_Infinitesimal_not_zero2)
   7.464  apply (frule_tac x = x in not_Infinitesimal_not_zero2)
   7.465 @@ -1364,7 +1361,7 @@
   7.466    fixes x h :: "'a::real_normed_div_algebra star"
   7.467    shows
   7.468       "[| x \<in> HFinite - Infinitesimal;
   7.469 -         h \<in> Infinitesimal |] ==> inverse(x + h) @= inverse x"
   7.470 +         h \<in> Infinitesimal |] ==> inverse(x + h) \<approx> inverse x"
   7.471  apply (auto intro: approx_inverse approx_sym Infinitesimal_add_approx_self)
   7.472  done
   7.473  
   7.474 @@ -1372,7 +1369,7 @@
   7.475    fixes x h :: "'a::real_normed_div_algebra star"
   7.476    shows
   7.477       "[| x \<in> HFinite - Infinitesimal;
   7.478 -         h \<in> Infinitesimal |] ==> inverse(h + x) @= inverse x"
   7.479 +         h \<in> Infinitesimal |] ==> inverse(h + x) \<approx> inverse x"
   7.480  apply (rule add.commute [THEN subst])
   7.481  apply (blast intro: inverse_add_Infinitesimal_approx)
   7.482  done
   7.483 @@ -1381,7 +1378,7 @@
   7.484    fixes x h :: "'a::real_normed_div_algebra star"
   7.485    shows
   7.486       "[| x \<in> HFinite - Infinitesimal;
   7.487 -         h \<in> Infinitesimal |] ==> inverse(x + h) - inverse x @= h"
   7.488 +         h \<in> Infinitesimal |] ==> inverse(x + h) - inverse x \<approx> h"
   7.489  apply (rule approx_trans2)
   7.490  apply (auto intro: inverse_add_Infinitesimal_approx
   7.491              simp add: mem_infmal_iff approx_minus_iff [symmetric])
   7.492 @@ -1411,7 +1408,7 @@
   7.493  
   7.494  lemma approx_HFinite_mult_cancel:
   7.495    fixes a w z :: "'a::real_normed_div_algebra star"
   7.496 -  shows "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
   7.497 +  shows "[| a: HFinite-Infinitesimal; a* w \<approx> a*z |] ==> w \<approx> z"
   7.498  apply safe
   7.499  apply (frule HFinite_inverse, assumption)
   7.500  apply (drule not_Infinitesimal_not_zero)
   7.501 @@ -1420,7 +1417,7 @@
   7.502  
   7.503  lemma approx_HFinite_mult_cancel_iff1:
   7.504    fixes a w z :: "'a::real_normed_div_algebra star"
   7.505 -  shows "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
   7.506 +  shows "a: HFinite-Infinitesimal ==> (a * w \<approx> a * z) = (w \<approx> z)"
   7.507  by (auto intro: approx_mult2 approx_HFinite_mult_cancel)
   7.508  
   7.509  lemma HInfinite_HFinite_add_cancel:
   7.510 @@ -1483,7 +1480,7 @@
   7.511  apply (simp (no_asm) add: HInfinite_HFinite_iff)
   7.512  done
   7.513  
   7.514 -lemma approx_hrabs_disj: "\<bar>x::hypreal\<bar> @= x \<or> \<bar>x\<bar> @= -x"
   7.515 +lemma approx_hrabs_disj: "\<bar>x::hypreal\<bar> \<approx> x \<or> \<bar>x\<bar> \<approx> -x"
   7.516  by (cut_tac x = x in hrabs_disj, auto)
   7.517  
   7.518  
   7.519 @@ -1514,36 +1511,36 @@
   7.520  by (simp add: monad_def)
   7.521  
   7.522  
   7.523 -subsection\<open>Proof that @{term "x @= y"} implies @{term"\<bar>x\<bar> @= \<bar>y\<bar>"}\<close>
   7.524 +subsection\<open>Proof that @{term "x \<approx> y"} implies @{term"\<bar>x\<bar> \<approx> \<bar>y\<bar>"}\<close>
   7.525  
   7.526 -lemma approx_subset_monad: "x @= y ==> {x,y} \<le> monad x"
   7.527 +lemma approx_subset_monad: "x \<approx> y ==> {x,y} \<le> monad x"
   7.528  apply (simp (no_asm))
   7.529  apply (simp add: approx_monad_iff)
   7.530  done
   7.531  
   7.532 -lemma approx_subset_monad2: "x @= y ==> {x,y} \<le> monad y"
   7.533 +lemma approx_subset_monad2: "x \<approx> y ==> {x,y} \<le> monad y"
   7.534  apply (drule approx_sym)
   7.535  apply (fast dest: approx_subset_monad)
   7.536  done
   7.537  
   7.538 -lemma mem_monad_approx: "u \<in> monad x ==> x @= u"
   7.539 +lemma mem_monad_approx: "u \<in> monad x ==> x \<approx> u"
   7.540  by (simp add: monad_def)
   7.541  
   7.542 -lemma approx_mem_monad: "x @= u ==> u \<in> monad x"
   7.543 +lemma approx_mem_monad: "x \<approx> u ==> u \<in> monad x"
   7.544  by (simp add: monad_def)
   7.545  
   7.546 -lemma approx_mem_monad2: "x @= u ==> x \<in> monad u"
   7.547 +lemma approx_mem_monad2: "x \<approx> u ==> x \<in> monad u"
   7.548  apply (simp add: monad_def)
   7.549  apply (blast intro!: approx_sym)
   7.550  done
   7.551  
   7.552 -lemma approx_mem_monad_zero: "[| x @= y;x \<in> monad 0 |] ==> y \<in> monad 0"
   7.553 +lemma approx_mem_monad_zero: "[| x \<approx> y;x \<in> monad 0 |] ==> y \<in> monad 0"
   7.554  apply (drule mem_monad_approx)
   7.555  apply (fast intro: approx_mem_monad approx_trans)
   7.556  done
   7.557  
   7.558  lemma Infinitesimal_approx_hrabs:
   7.559 -     "[| x @= y; (x::hypreal) \<in> Infinitesimal |] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
   7.560 +     "[| x \<approx> y; (x::hypreal) \<in> Infinitesimal |] ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
   7.561  apply (drule Infinitesimal_monad_zero_iff [THEN iffD1])
   7.562  apply (blast intro: approx_mem_monad_zero monad_zero_hrabs_iff [THEN iffD1] mem_monad_approx approx_trans3)
   7.563  done
   7.564 @@ -1570,32 +1567,32 @@
   7.565  done
   7.566  
   7.567  lemma lemma_approx_gt_zero:
   7.568 -     "[|0 < (x::hypreal); x \<notin> Infinitesimal; x @= y|] ==> 0 < y"
   7.569 +     "[|0 < (x::hypreal); x \<notin> Infinitesimal; x \<approx> y|] ==> 0 < y"
   7.570  by (blast dest: Ball_mem_monad_gt_zero approx_subset_monad)
   7.571  
   7.572  lemma lemma_approx_less_zero:
   7.573 -     "[|(x::hypreal) < 0; x \<notin> Infinitesimal; x @= y|] ==> y < 0"
   7.574 +     "[|(x::hypreal) < 0; x \<notin> Infinitesimal; x \<approx> y|] ==> y < 0"
   7.575  by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
   7.576  
   7.577 -theorem approx_hrabs: "(x::hypreal) @= y ==> \<bar>x\<bar> @= \<bar>y\<bar>"
   7.578 +theorem approx_hrabs: "(x::hypreal) \<approx> y ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
   7.579  by (drule approx_hnorm, simp)
   7.580  
   7.581 -lemma approx_hrabs_zero_cancel: "\<bar>x::hypreal\<bar> @= 0 ==> x @= 0"
   7.582 +lemma approx_hrabs_zero_cancel: "\<bar>x::hypreal\<bar> \<approx> 0 ==> x \<approx> 0"
   7.583  apply (cut_tac x = x in hrabs_disj)
   7.584  apply (auto dest: approx_minus)
   7.585  done
   7.586  
   7.587  lemma approx_hrabs_add_Infinitesimal:
   7.588 -  "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> @= \<bar>x + e\<bar>"
   7.589 +  "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> \<approx> \<bar>x + e\<bar>"
   7.590  by (fast intro: approx_hrabs Infinitesimal_add_approx_self)
   7.591  
   7.592  lemma approx_hrabs_add_minus_Infinitesimal:
   7.593 -     "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> @= \<bar>x + -e\<bar>"
   7.594 +     "(e::hypreal) \<in> Infinitesimal ==> \<bar>x\<bar> \<approx> \<bar>x + -e\<bar>"
   7.595  by (fast intro: approx_hrabs Infinitesimal_add_minus_approx_self)
   7.596  
   7.597  lemma hrabs_add_Infinitesimal_cancel:
   7.598       "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
   7.599 -         \<bar>x + e\<bar> = \<bar>y + e'\<bar>|] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
   7.600 +         \<bar>x + e\<bar> = \<bar>y + e'\<bar>|] ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
   7.601  apply (drule_tac x = x in approx_hrabs_add_Infinitesimal)
   7.602  apply (drule_tac x = y in approx_hrabs_add_Infinitesimal)
   7.603  apply (auto intro: approx_trans2)
   7.604 @@ -1603,7 +1600,7 @@
   7.605  
   7.606  lemma hrabs_add_minus_Infinitesimal_cancel:
   7.607       "[| (e::hypreal) \<in> Infinitesimal; e' \<in> Infinitesimal;
   7.608 -         \<bar>x + -e\<bar> = \<bar>y + -e'\<bar>|] ==> \<bar>x\<bar> @= \<bar>y\<bar>"
   7.609 +         \<bar>x + -e\<bar> = \<bar>y + -e'\<bar>|] ==> \<bar>x\<bar> \<approx> \<bar>y\<bar>"
   7.610  apply (drule_tac x = x in approx_hrabs_add_minus_Infinitesimal)
   7.611  apply (drule_tac x = y in approx_hrabs_add_minus_Infinitesimal)
   7.612  apply (auto intro: approx_trans2)
   7.613 @@ -1755,7 +1752,7 @@
   7.614  
   7.615  subsection\<open>Theorems about Standard Part\<close>
   7.616  
   7.617 -lemma st_approx_self: "x \<in> HFinite ==> st x @= x"
   7.618 +lemma st_approx_self: "x \<in> HFinite ==> st x \<approx> x"
   7.619  apply (simp add: st_def)
   7.620  apply (frule st_part_Ex, safe)
   7.621  apply (rule someI2)
   7.622 @@ -1786,14 +1783,14 @@
   7.623  lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
   7.624  by (rule SReal_hypreal_of_real [THEN st_SReal_eq])
   7.625  
   7.626 -lemma st_eq_approx: "[| x \<in> HFinite; y \<in> HFinite; st x = st y |] ==> x @= y"
   7.627 +lemma st_eq_approx: "[| x \<in> HFinite; y \<in> HFinite; st x = st y |] ==> x \<approx> y"
   7.628  by (auto dest!: st_approx_self elim!: approx_trans3)
   7.629  
   7.630  lemma approx_st_eq:
   7.631 -  assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x @= y"
   7.632 +  assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x \<approx> y"
   7.633    shows "st x = st y"
   7.634  proof -
   7.635 -  have "st x @= x" "st y @= y" "st x \<in> \<real>" "st y \<in> \<real>"
   7.636 +  have "st x \<approx> x" "st y \<approx> y" "st x \<in> \<real>" "st y \<in> \<real>"
   7.637      by (simp_all add: st_approx_self st_SReal x y)
   7.638    with xy show ?thesis
   7.639      by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
   7.640 @@ -1801,7 +1798,7 @@
   7.641  
   7.642  lemma st_eq_approx_iff:
   7.643       "[| x \<in> HFinite; y \<in> HFinite|]
   7.644 -                   ==> (x @= y) = (st x = st y)"
   7.645 +                   ==> (x \<approx> y) = (st x = st y)"
   7.646  by (blast intro: approx_st_eq st_eq_approx)
   7.647  
   7.648  lemma st_Infinitesimal_add_SReal:
   7.649 @@ -2120,12 +2117,12 @@
   7.650  lemma HFinite_epsilon [simp]: "\<epsilon> \<in> HFinite"
   7.651  by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
   7.652  
   7.653 -lemma epsilon_approx_zero [simp]: "\<epsilon> @= 0"
   7.654 +lemma epsilon_approx_zero [simp]: "\<epsilon> \<approx> 0"
   7.655  apply (simp (no_asm) add: mem_infmal_iff [symmetric])
   7.656  done
   7.657  
   7.658  (*------------------------------------------------------------------------
   7.659 -  Needed for proof that we define a hyperreal [<X(n)] @= hypreal_of_real a given
   7.660 +  Needed for proof that we define a hyperreal [<X(n)] \<approx> hypreal_of_real a given
   7.661    that \<forall>n. |X n - a| < 1/n. Used in proof of NSLIM => LIM.
   7.662   -----------------------------------------------------------------------*)
   7.663  
   7.664 @@ -2204,12 +2201,12 @@
   7.665  
   7.666  lemma real_seq_to_hypreal_approx:
   7.667       "\<forall>n. norm(X n - x) < inverse(real(Suc n))
   7.668 -      ==> star_n X @= star_of x"
   7.669 +      ==> star_n X \<approx> star_of x"
   7.670  by (metis bex_Infinitesimal_iff real_seq_to_hypreal_Infinitesimal)
   7.671  
   7.672  lemma real_seq_to_hypreal_approx2:
   7.673       "\<forall>n. norm(x - X n) < inverse(real(Suc n))
   7.674 -               ==> star_n X @= star_of x"
   7.675 +               ==> star_n X \<approx> star_of x"
   7.676  by (metis norm_minus_commute real_seq_to_hypreal_approx)
   7.677  
   7.678  lemma real_seq_to_hypreal_Infinitesimal2:
     8.1 --- a/src/HOL/NSA/NSCA.thy	Wed Dec 30 17:55:43 2015 +0100
     8.2 +++ b/src/HOL/NSA/NSCA.thy	Wed Dec 30 18:03:23 2015 +0100
     8.3 @@ -16,7 +16,7 @@
     8.4  
     8.5  definition \<comment>\<open>standard part map\<close>
     8.6    stc :: "hcomplex => hcomplex" where 
     8.7 -  "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
     8.8 +  "stc x = (SOME r. x \<in> HFinite & r:SComplex & r \<approx> x)"
     8.9  
    8.10  
    8.11  subsection\<open>Closure Laws for SComplex, the Standard Complex Numbers\<close>
    8.12 @@ -124,52 +124,52 @@
    8.13  subsection\<open>The ``Infinitely Close'' Relation\<close>
    8.14  
    8.15  (*
    8.16 -Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)"
    8.17 +Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z \<approx> hcmod w)"
    8.18  by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff]));
    8.19  *)
    8.20  
    8.21  lemma approx_SComplex_mult_cancel_zero:
    8.22 -     "[| a \<in> SComplex; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
    8.23 +     "[| a \<in> SComplex; a \<noteq> 0; a*x \<approx> 0 |] ==> x \<approx> 0"
    8.24  apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])
    8.25  apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
    8.26  done
    8.27  
    8.28 -lemma approx_mult_SComplex1: "[| a \<in> SComplex; x @= 0 |] ==> x*a @= 0"
    8.29 +lemma approx_mult_SComplex1: "[| a \<in> SComplex; x \<approx> 0 |] ==> x*a \<approx> 0"
    8.30  by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult1)
    8.31  
    8.32 -lemma approx_mult_SComplex2: "[| a \<in> SComplex; x @= 0 |] ==> a*x @= 0"
    8.33 +lemma approx_mult_SComplex2: "[| a \<in> SComplex; x \<approx> 0 |] ==> a*x \<approx> 0"
    8.34  by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult2)
    8.35  
    8.36  lemma approx_mult_SComplex_zero_cancel_iff [simp]:
    8.37 -     "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
    8.38 +     "[|a \<in> SComplex; a \<noteq> 0 |] ==> (a*x \<approx> 0) = (x \<approx> 0)"
    8.39  by (blast intro: approx_SComplex_mult_cancel_zero approx_mult_SComplex2)
    8.40  
    8.41  lemma approx_SComplex_mult_cancel:
    8.42 -     "[| a \<in> SComplex; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
    8.43 +     "[| a \<in> SComplex; a \<noteq> 0; a* w \<approx> a*z |] ==> w \<approx> z"
    8.44  apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]])
    8.45  apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
    8.46  done
    8.47  
    8.48  lemma approx_SComplex_mult_cancel_iff1 [simp]:
    8.49 -     "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
    8.50 +     "[| a \<in> SComplex; a \<noteq> 0|] ==> (a* w \<approx> a*z) = (w \<approx> z)"
    8.51  by (auto intro!: approx_mult2 Standard_subset_HFinite [THEN subsetD]
    8.52              intro: approx_SComplex_mult_cancel)
    8.53  
    8.54  (* TODO: generalize following theorems: hcmod -> hnorm *)
    8.55  
    8.56 -lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)"
    8.57 +lemma approx_hcmod_approx_zero: "(x \<approx> y) = (hcmod (y - x) \<approx> 0)"
    8.58  apply (subst hnorm_minus_commute)
    8.59  apply (simp add: approx_def Infinitesimal_hcmod_iff)
    8.60  done
    8.61  
    8.62 -lemma approx_approx_zero_iff: "(x @= 0) = (hcmod x @= 0)"
    8.63 +lemma approx_approx_zero_iff: "(x \<approx> 0) = (hcmod x \<approx> 0)"
    8.64  by (simp add: approx_hcmod_approx_zero)
    8.65  
    8.66 -lemma approx_minus_zero_cancel_iff [simp]: "(-x @= 0) = (x @= 0)"
    8.67 +lemma approx_minus_zero_cancel_iff [simp]: "(-x \<approx> 0) = (x \<approx> 0)"
    8.68  by (simp add: approx_def)
    8.69  
    8.70  lemma Infinitesimal_hcmod_add_diff:
    8.71 -     "u @= 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
    8.72 +     "u \<approx> 0 ==> hcmod(x + u) - hcmod x \<in> Infinitesimal"
    8.73  apply (drule approx_approx_zero_iff [THEN iffD1])
    8.74  apply (rule_tac e = "hcmod u" and e' = "- hcmod u" in Infinitesimal_interval2)
    8.75  apply (auto simp add: mem_infmal_iff [symmetric])
    8.76 @@ -177,7 +177,7 @@
    8.77  apply auto
    8.78  done
    8.79  
    8.80 -lemma approx_hcmod_add_hcmod: "u @= 0 ==> hcmod(x + u) @= hcmod x"
    8.81 +lemma approx_hcmod_add_hcmod: "u \<approx> 0 ==> hcmod(x + u) \<approx> hcmod x"
    8.82  apply (rule approx_minus_iff [THEN iffD2])
    8.83  apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric])
    8.84  done
    8.85 @@ -210,11 +210,11 @@
    8.86  by (fast dest: Standard_numeral [THEN SComplex_Infinitesimal_zero])
    8.87  
    8.88  lemma approx_SComplex_not_zero:
    8.89 -     "[| y \<in> SComplex; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
    8.90 +     "[| y \<in> SComplex; x \<approx> y; y\<noteq> 0 |] ==> x \<noteq> 0"
    8.91  by (auto dest: SComplex_Infinitesimal_zero approx_sym [THEN mem_infmal_iff [THEN iffD2]])
    8.92  
    8.93  lemma SComplex_approx_iff:
    8.94 -     "[|x \<in> SComplex; y \<in> SComplex|] ==> (x @= y) = (x = y)"
    8.95 +     "[|x \<in> SComplex; y \<in> SComplex|] ==> (x \<approx> y) = (x = y)"
    8.96  by (auto simp add: Standard_def)
    8.97  
    8.98  lemma numeral_Infinitesimal_iff [simp]:
    8.99 @@ -226,7 +226,7 @@
   8.100  done
   8.101  
   8.102  lemma approx_unique_complex:
   8.103 -     "[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s"
   8.104 +     "[| r \<in> SComplex; s \<in> SComplex; r \<approx> x; s \<approx> x|] ==> r = s"
   8.105  by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2)
   8.106  
   8.107  subsection \<open>Properties of @{term hRe}, @{term hIm} and @{term HComplex}\<close>
   8.108 @@ -335,7 +335,7 @@
   8.109  by (simp add: HInfinite_HFinite_iff hcomplex_HFinite_iff)
   8.110  
   8.111  lemma hcomplex_of_hypreal_approx_iff [simp]:
   8.112 -     "(hcomplex_of_hypreal x @= hcomplex_of_hypreal z) = (x @= z)"
   8.113 +     "(hcomplex_of_hypreal x \<approx> hcomplex_of_hypreal z) = (x \<approx> z)"
   8.114  by (simp add: hcomplex_approx_iff)
   8.115  
   8.116  lemma Standard_HComplex:
   8.117 @@ -343,14 +343,14 @@
   8.118  by (simp add: HComplex_def)
   8.119  
   8.120  (* Here we go - easy proof now!! *)
   8.121 -lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x @= t"
   8.122 +lemma stc_part_Ex: "x:HFinite ==> \<exists>t \<in> SComplex. x \<approx> t"
   8.123  apply (simp add: hcomplex_HFinite_iff hcomplex_approx_iff)
   8.124  apply (rule_tac x="HComplex (st (hRe x)) (st (hIm x))" in bexI)
   8.125  apply (simp add: st_approx_self [THEN approx_sym])
   8.126  apply (simp add: Standard_HComplex st_SReal [unfolded Reals_eq_Standard])
   8.127  done
   8.128  
   8.129 -lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex &  x @= t"
   8.130 +lemma stc_part_Ex1: "x:HFinite ==> EX! t. t \<in> SComplex &  x \<approx> t"
   8.131  apply (drule stc_part_Ex, safe)
   8.132  apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
   8.133  apply (auto intro!: approx_unique_complex)
   8.134 @@ -368,7 +368,7 @@
   8.135  
   8.136  subsection\<open>Theorems About Standard Part\<close>
   8.137  
   8.138 -lemma stc_approx_self: "x \<in> HFinite ==> stc x @= x"
   8.139 +lemma stc_approx_self: "x \<in> HFinite ==> stc x \<approx> x"
   8.140  apply (simp add: stc_def)
   8.141  apply (frule stc_part_Ex, safe)
   8.142  apply (rule someI2)
   8.143 @@ -403,16 +403,16 @@
   8.144  by auto
   8.145  
   8.146  lemma stc_eq_approx:
   8.147 -     "[| x \<in> HFinite; y \<in> HFinite; stc x = stc y |] ==> x @= y"
   8.148 +     "[| x \<in> HFinite; y \<in> HFinite; stc x = stc y |] ==> x \<approx> y"
   8.149  by (auto dest!: stc_approx_self elim!: approx_trans3)
   8.150  
   8.151  lemma approx_stc_eq:
   8.152 -     "[| x \<in> HFinite; y \<in> HFinite; x @= y |] ==> stc x = stc y"
   8.153 +     "[| x \<in> HFinite; y \<in> HFinite; x \<approx> y |] ==> stc x = stc y"
   8.154  by (blast intro: approx_trans approx_trans2 SComplex_approx_iff [THEN iffD1]
   8.155            dest: stc_approx_self stc_SComplex)
   8.156  
   8.157  lemma stc_eq_approx_iff:
   8.158 -     "[| x \<in> HFinite; y \<in> HFinite|] ==> (x @= y) = (stc x = stc y)"
   8.159 +     "[| x \<in> HFinite; y \<in> HFinite|] ==> (x \<approx> y) = (stc x = stc y)"
   8.160  by (blast intro: approx_stc_eq stc_eq_approx)
   8.161  
   8.162  lemma stc_Infinitesimal_add_SComplex:
     9.1 --- a/src/HOL/NSA/Star.thy	Wed Dec 30 17:55:43 2015 +0100
     9.2 +++ b/src/HOL/NSA/Star.thy	Wed Dec 30 18:03:23 2015 +0100
     9.3 @@ -189,7 +189,7 @@
     9.4  
     9.5  (* this is trivial, given starfun_Id *)
     9.6  lemma starfun_Idfun_approx:
     9.7 -  "x @= star_of a ==> ( *f* (%x. x)) x @= star_of a"
     9.8 +  "x \<approx> star_of a ==> ( *f* (%x. x)) x \<approx> star_of a"
     9.9  by (simp only: starfun_Id)
    9.10  
    9.11  text\<open>The Star-function is a (nonstandard) extension of the function\<close>
    9.12 @@ -224,7 +224,7 @@
    9.13  lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
    9.14  by (rule starfun_star_of)
    9.15  
    9.16 -lemma starfun_approx: "( *f* f) (star_of a) @= star_of (f a)"
    9.17 +lemma starfun_approx: "( *f* f) (star_of a) \<approx> star_of (f a)"
    9.18  by simp
    9.19  
    9.20  (* useful for NS definition of derivatives *)
    9.21 @@ -238,15 +238,15 @@
    9.22  
    9.23  lemma starfun_mult_HFinite_approx:
    9.24    fixes l m :: "'a::real_normed_algebra star"
    9.25 -  shows "[| ( *f* f) x @= l; ( *f* g) x @= m;
    9.26 +  shows "[| ( *f* f) x \<approx> l; ( *f* g) x \<approx> m;
    9.27                    l: HFinite; m: HFinite
    9.28 -               |] ==>  ( *f* (%x. f x * g x)) x @= l * m"
    9.29 +               |] ==>  ( *f* (%x. f x * g x)) x \<approx> l * m"
    9.30  apply (drule (3) approx_mult_HFinite)
    9.31  apply (auto intro: approx_HFinite [OF _ approx_sym])
    9.32  done
    9.33  
    9.34 -lemma starfun_add_approx: "[| ( *f* f) x @= l; ( *f* g) x @= m
    9.35 -               |] ==>  ( *f* (%x. f x + g x)) x @= l + m"
    9.36 +lemma starfun_add_approx: "[| ( *f* f) x \<approx> l; ( *f* g) x \<approx> m
    9.37 +               |] ==>  ( *f* (%x. f x + g x)) x \<approx> l + m"
    9.38  by (auto intro: approx_add)
    9.39  
    9.40  text\<open>Examples: hrabs is nonstandard extension of rabs
    9.41 @@ -298,7 +298,7 @@
    9.42         {x. \<bar>( *f* f) x + -star_of y\<bar> < star_of r}"
    9.43  by (transfer, rule refl)
    9.44  
    9.45 -text\<open>Another characterization of Infinitesimal and one of @= relation.
    9.46 +text\<open>Another characterization of Infinitesimal and one of \<open>\<approx>\<close> relation.
    9.47     In this theory since \<open>hypreal_hrabs\<close> proved here. Maybe
    9.48     move both theorems??\<close>
    9.49  lemma Infinitesimal_FreeUltrafilterNat_iff2:
    9.50 @@ -317,7 +317,7 @@
    9.51  apply (auto elim!: eventually_mono)
    9.52  done
    9.53  
    9.54 -lemma approx_FreeUltrafilterNat_iff: "star_n X @= star_n Y =
    9.55 +lemma approx_FreeUltrafilterNat_iff: "star_n X \<approx> star_n Y =
    9.56        (\<forall>r>0. eventually (\<lambda>n. norm (X n - Y n) < r) \<U>)"
    9.57  apply (subst approx_minus_iff)
    9.58  apply (rule mem_infmal_iff [THEN subst])
    9.59 @@ -325,7 +325,7 @@
    9.60  apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
    9.61  done
    9.62  
    9.63 -lemma approx_FreeUltrafilterNat_iff2: "star_n X @= star_n Y =
    9.64 +lemma approx_FreeUltrafilterNat_iff2: "star_n X \<approx> star_n Y =
    9.65        (\<forall>m. eventually (\<lambda>n. norm (X n - Y n) < inverse(real(Suc m))) \<U>)"
    9.66  apply (subst approx_minus_iff)
    9.67  apply (rule mem_infmal_iff [THEN subst])