prefer symbols;
authorwenzelm
Mon Aug 31 21:28:08 2015 +0200 (2015-08-31)
changeset 61070b72a990adfe2
parent 61069 aefe89038dd2
child 61071 c6ac3c3fbb85
prefer symbols;
src/HOL/Archimedean_Field.thy
src/HOL/Int.thy
src/HOL/Library/Convex.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/NSCA.thy
src/HOL/NSA/Star.thy
src/HOL/Nat.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Mon Aug 31 21:01:21 2015 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Mon Aug 31 21:28:08 2015 +0200
     1.3 @@ -546,14 +546,14 @@
     1.4  lemma frac_lt_1: "frac x < 1"
     1.5    by  (simp add: frac_def) linarith
     1.6  
     1.7 -lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> Ints"
     1.8 +lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> \<int>"
     1.9    by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int )
    1.10  
    1.11  lemma frac_ge_0 [simp]: "frac x \<ge> 0"
    1.12    unfolding frac_def
    1.13    by linarith
    1.14  
    1.15 -lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> Ints"
    1.16 +lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> \<int>"
    1.17    by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl)
    1.18  
    1.19  lemma frac_of_int [simp]: "frac (of_int z) = 0"
    1.20 @@ -582,7 +582,7 @@
    1.21  
    1.22  lemma frac_unique_iff:
    1.23    fixes x :: "'a::floor_ceiling"
    1.24 -  shows  "(frac x) = a \<longleftrightarrow> x - a \<in> Ints \<and> 0 \<le> a \<and> a < 1"
    1.25 +  shows  "(frac x) = a \<longleftrightarrow> x - a \<in> \<int> \<and> 0 \<le> a \<and> a < 1"
    1.26    apply (auto simp: Ints_def frac_def)
    1.27    apply linarith
    1.28    apply linarith
    1.29 @@ -593,7 +593,7 @@
    1.30    
    1.31  lemma frac_neg:
    1.32    fixes x :: "'a::floor_ceiling"
    1.33 -  shows  "frac (-x) = (if x \<in> Ints then 0 else 1 - frac x)"
    1.34 +  shows  "frac (-x) = (if x \<in> \<int> then 0 else 1 - frac x)"
    1.35    apply (auto simp add: frac_unique_iff)
    1.36    apply (simp add: frac_def)
    1.37    by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
     2.1 --- a/src/HOL/Int.thy	Mon Aug 31 21:01:21 2015 +0200
     2.2 +++ b/src/HOL/Int.thy	Mon Aug 31 21:28:08 2015 +0200
     2.3 @@ -623,11 +623,8 @@
     2.4  context ring_1
     2.5  begin
     2.6  
     2.7 -definition Ints  :: "'a set" where
     2.8 -  "Ints = range of_int"
     2.9 -
    2.10 -notation (xsymbols)
    2.11 -  Ints  ("\<int>")
    2.12 +definition Ints :: "'a set"  ("\<int>")
    2.13 +  where "\<int> = range of_int"
    2.14  
    2.15  lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
    2.16    by (simp add: Ints_def)
    2.17 @@ -687,7 +684,7 @@
    2.18  text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
    2.19  
    2.20  lemma Ints_double_eq_0_iff:
    2.21 -  assumes in_Ints: "a \<in> Ints"
    2.22 +  assumes in_Ints: "a \<in> \<int>"
    2.23    shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
    2.24  proof -
    2.25    from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
    2.26 @@ -706,7 +703,7 @@
    2.27  qed
    2.28  
    2.29  lemma Ints_odd_nonzero:
    2.30 -  assumes in_Ints: "a \<in> Ints"
    2.31 +  assumes in_Ints: "a \<in> \<int>"
    2.32    shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
    2.33  proof -
    2.34    from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
    2.35 @@ -720,11 +717,11 @@
    2.36    qed
    2.37  qed
    2.38  
    2.39 -lemma Nats_numeral [simp]: "numeral w \<in> Nats"
    2.40 +lemma Nats_numeral [simp]: "numeral w \<in> \<nat>"
    2.41    using of_nat_in_Nats [of "numeral w"] by simp
    2.42  
    2.43  lemma Ints_odd_less_0:
    2.44 -  assumes in_Ints: "a \<in> Ints"
    2.45 +  assumes in_Ints: "a \<in> \<int>"
    2.46    shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
    2.47  proof -
    2.48    from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
     3.1 --- a/src/HOL/Library/Convex.thy	Mon Aug 31 21:01:21 2015 +0200
     3.2 +++ b/src/HOL/Library/Convex.thy	Mon Aug 31 21:28:08 2015 +0200
     3.3 @@ -137,7 +137,7 @@
     3.4      by (simp only: convex_Int 3 4)
     3.5  qed
     3.6  
     3.7 -lemma convex_Reals: "convex Reals"
     3.8 +lemma convex_Reals: "convex \<real>"
     3.9    by (simp add: convex_def scaleR_conv_of_real)
    3.10  
    3.11  
     4.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Aug 31 21:01:21 2015 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Aug 31 21:28:08 2015 +0200
     4.3 @@ -242,9 +242,9 @@
     4.4    by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
     4.5              isCont_Im continuous_ident continuous_const)+
     4.6  
     4.7 -lemma closed_complex_Reals: "closed (Reals :: complex set)"
     4.8 +lemma closed_complex_Reals: "closed (\<real> :: complex set)"
     4.9  proof -
    4.10 -  have "(Reals :: complex set) = {z. Im z = 0}"
    4.11 +  have "(\<real> :: complex set) = {z. Im z = 0}"
    4.12      by (auto simp: complex_is_Real_iff)
    4.13    then show ?thesis
    4.14      by (metis closed_halfspace_Im_eq)
     5.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Aug 31 21:01:21 2015 +0200
     5.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Aug 31 21:28:08 2015 +0200
     5.3 @@ -211,7 +211,7 @@
     5.4    by (auto simp: exp_eq abs_mult)
     5.5  
     5.6  lemma exp_integer_2pi:
     5.7 -  assumes "n \<in> Ints"
     5.8 +  assumes "n \<in> \<int>"
     5.9    shows "exp((2 * n * pi) * ii) = 1"
    5.10  proof -
    5.11    have "exp((2 * n * pi) * ii) = exp 0"
    5.12 @@ -751,15 +751,15 @@
    5.13      by blast
    5.14  qed
    5.15  
    5.16 -lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z"
    5.17 +lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
    5.18  proof (cases "z=0")
    5.19    case True then show ?thesis
    5.20      by simp
    5.21  next
    5.22    case False
    5.23 -  have "z \<in> Reals \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
    5.24 +  have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
    5.25      by (metis Arg_eq)
    5.26 -  also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
    5.27 +  also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
    5.28      using False
    5.29      by (simp add: zero_le_mult_iff)
    5.30    also have "... \<longleftrightarrow> Arg z = 0"
    5.31 @@ -955,7 +955,7 @@
    5.32  corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
    5.33    by (simp add: Ln_of_real)
    5.34  
    5.35 -lemma cmod_Ln_Reals [simp]: "z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
    5.36 +lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
    5.37    using Ln_of_real by force
    5.38  
    5.39  lemma Ln_1: "ln 1 = (0::complex)"
    5.40 @@ -1565,10 +1565,10 @@
    5.41    using lim_Ln_over_power [of 1]
    5.42    by simp
    5.43  
    5.44 -lemma Ln_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
    5.45 +lemma Ln_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
    5.46    using Ln_of_real by force
    5.47  
    5.48 -lemma powr_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
    5.49 +lemma powr_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
    5.50    by (simp add: powr_of_real)
    5.51  
    5.52  lemma lim_ln_over_power:
     6.1 --- a/src/HOL/NSA/HyperDef.thy	Mon Aug 31 21:01:21 2015 +0200
     6.2 +++ b/src/HOL/NSA/HyperDef.thy	Mon Aug 31 21:28:08 2015 +0200
     6.3 @@ -103,7 +103,7 @@
     6.4      by transfer simp
     6.5  qed
     6.6  
     6.7 -lemma Reals_eq_Standard: "(Reals :: hypreal set) = Standard"
     6.8 +lemma Reals_eq_Standard: "(\<real> :: hypreal set) = Standard"
     6.9  by (simp add: Reals_def Standard_def)
    6.10  
    6.11  
    6.12 @@ -539,7 +539,7 @@
    6.13  by transfer (rule refl)
    6.14  
    6.15  lemma hyperpow_SReal [simp]:
    6.16 -     "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
    6.17 +     "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> \<real>"
    6.18  by (simp add: Reals_eq_Standard)
    6.19  
    6.20  lemma hyperpow_zero_HNatInfinite [simp]:
     7.1 --- a/src/HOL/NSA/NSA.thy	Mon Aug 31 21:01:21 2015 +0200
     7.2 +++ b/src/HOL/NSA/NSA.thy	Mon Aug 31 21:28:08 2015 +0200
     7.3 @@ -33,7 +33,7 @@
     7.4  definition
     7.5    st        :: "hypreal => hypreal" where
     7.6      --{*the standard part of a hyperreal*}
     7.7 -  "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
     7.8 +  "st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r @= x)"
     7.9  
    7.10  definition
    7.11    monad     :: "'a::real_normed_vector star => 'a star set" where
    7.12 @@ -49,7 +49,7 @@
    7.13  notation (HTML output)
    7.14    approx  (infixl "\<approx>" 50)
    7.15  
    7.16 -lemma SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
    7.17 +lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}"
    7.18  by (simp add: Reals_def image_def)
    7.19  
    7.20  subsection {* Nonstandard Extension of the Norm Function *}
    7.21 @@ -176,54 +176,54 @@
    7.22  
    7.23  subsection{*Closure Laws for the Standard Reals*}
    7.24  
    7.25 -lemma Reals_minus_iff [simp]: "(-x \<in> Reals) = (x \<in> Reals)"
    7.26 +lemma Reals_minus_iff [simp]: "(-x \<in> \<real>) = (x \<in> \<real>)"
    7.27  apply auto
    7.28  apply (drule Reals_minus, auto)
    7.29  done
    7.30  
    7.31 -lemma Reals_add_cancel: "\<lbrakk>x + y \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
    7.32 +lemma Reals_add_cancel: "\<lbrakk>x + y \<in> \<real>; y \<in> \<real>\<rbrakk> \<Longrightarrow> x \<in> \<real>"
    7.33  by (drule (1) Reals_diff, simp)
    7.34  
    7.35 -lemma SReal_hrabs: "(x::hypreal) \<in> Reals ==> abs x \<in> Reals"
    7.36 +lemma SReal_hrabs: "(x::hypreal) \<in> \<real> ==> abs x \<in> \<real>"
    7.37  by (simp add: Reals_eq_Standard)
    7.38  
    7.39 -lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals"
    7.40 +lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> \<real>"
    7.41  by (simp add: Reals_eq_Standard)
    7.42  
    7.43 -lemma SReal_divide_numeral: "r \<in> Reals ==> r/(numeral w::hypreal) \<in> Reals"
    7.44 +lemma SReal_divide_numeral: "r \<in> \<real> ==> r/(numeral w::hypreal) \<in> \<real>"
    7.45  by simp
    7.46  
    7.47  text{*epsilon is not in Reals because it is an infinitesimal*}
    7.48 -lemma SReal_epsilon_not_mem: "epsilon \<notin> Reals"
    7.49 +lemma SReal_epsilon_not_mem: "epsilon \<notin> \<real>"
    7.50  apply (simp add: SReal_def)
    7.51  apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym])
    7.52  done
    7.53  
    7.54 -lemma SReal_omega_not_mem: "omega \<notin> Reals"
    7.55 +lemma SReal_omega_not_mem: "omega \<notin> \<real>"
    7.56  apply (simp add: SReal_def)
    7.57  apply (auto simp add: hypreal_of_real_not_eq_omega [THEN not_sym])
    7.58  done
    7.59  
    7.60 -lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> Reals} = (UNIV::real set)"
    7.61 +lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> \<real>} = (UNIV::real set)"
    7.62  by simp
    7.63  
    7.64 -lemma SReal_iff: "(x \<in> Reals) = (\<exists>y. x = hypreal_of_real y)"
    7.65 +lemma SReal_iff: "(x \<in> \<real>) = (\<exists>y. x = hypreal_of_real y)"
    7.66  by (simp add: SReal_def)
    7.67  
    7.68 -lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = Reals"
    7.69 +lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = \<real>"
    7.70  by (simp add: Reals_eq_Standard Standard_def)
    7.71  
    7.72 -lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` Reals = UNIV"
    7.73 +lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` \<real> = UNIV"
    7.74  apply (auto simp add: SReal_def)
    7.75  apply (rule inj_star_of [THEN inv_f_f, THEN subst], blast)
    7.76  done
    7.77  
    7.78  lemma SReal_hypreal_of_real_image:
    7.79 -      "[| \<exists>x. x: P; P \<subseteq> Reals |] ==> \<exists>Q. P = hypreal_of_real ` Q"
    7.80 +      "[| \<exists>x. x: P; P \<subseteq> \<real> |] ==> \<exists>Q. P = hypreal_of_real ` Q"
    7.81  by (simp add: SReal_def image_def, blast)
    7.82  
    7.83  lemma SReal_dense:
    7.84 -     "[| (x::hypreal) \<in> Reals; y \<in> Reals;  x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
    7.85 +     "[| (x::hypreal) \<in> \<real>; y \<in> \<real>;  x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
    7.86  apply (auto simp add: SReal_def)
    7.87  apply (drule dense, auto)
    7.88  done
    7.89 @@ -231,12 +231,12 @@
    7.90  text{*Completeness of Reals, but both lemmas are unused.*}
    7.91  
    7.92  lemma SReal_sup_lemma:
    7.93 -     "P \<subseteq> Reals ==> ((\<exists>x \<in> P. y < x) =
    7.94 +     "P \<subseteq> \<real> ==> ((\<exists>x \<in> P. y < x) =
    7.95        (\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))"
    7.96  by (blast dest!: SReal_iff [THEN iffD1])
    7.97  
    7.98  lemma SReal_sup_lemma2:
    7.99 -     "[| P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
   7.100 +     "[| P \<subseteq> \<real>; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
   7.101        ==> (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) &
   7.102            (\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)"
   7.103  apply (rule conjI)
   7.104 @@ -277,7 +277,7 @@
   7.105  apply (blast intro: Reals_add SReal_hypreal_of_real Reals_1)
   7.106  done
   7.107  
   7.108 -lemma SReal_subset_HFinite: "(Reals::hypreal set) \<subseteq> HFinite"
   7.109 +lemma SReal_subset_HFinite: "(\<real>::hypreal set) \<subseteq> HFinite"
   7.110  by (auto simp add: SReal_def)
   7.111  
   7.112  lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. hnorm x < t"
   7.113 @@ -850,29 +850,29 @@
   7.114  by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
   7.115  
   7.116  lemma approx_SReal_mult_cancel_zero:
   7.117 -     "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
   7.118 +     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
   7.119  apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   7.120  apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   7.121  done
   7.122  
   7.123 -lemma approx_mult_SReal1: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> x*a @= 0"
   7.124 +lemma approx_mult_SReal1: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> x*a @= 0"
   7.125  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
   7.126  
   7.127 -lemma approx_mult_SReal2: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> a*x @= 0"
   7.128 +lemma approx_mult_SReal2: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> a*x @= 0"
   7.129  by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
   7.130  
   7.131  lemma approx_mult_SReal_zero_cancel_iff [simp]:
   7.132 -     "[|(a::hypreal) \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
   7.133 +     "[|(a::hypreal) \<in> \<real>; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
   7.134  by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
   7.135  
   7.136  lemma approx_SReal_mult_cancel:
   7.137 -     "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
   7.138 +     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
   7.139  apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   7.140  apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
   7.141  done
   7.142  
   7.143  lemma approx_SReal_mult_cancel_iff1 [simp]:
   7.144 -     "[| (a::hypreal) \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
   7.145 +     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
   7.146  by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
   7.147           intro: approx_SReal_mult_cancel)
   7.148  
   7.149 @@ -907,7 +907,7 @@
   7.150  subsection{* Zero is the Only Infinitesimal that is also a Real*}
   7.151  
   7.152  lemma Infinitesimal_less_SReal:
   7.153 -     "[| (x::hypreal) \<in> Reals; y \<in> Infinitesimal; 0 < x |] ==> y < x"
   7.154 +     "[| (x::hypreal) \<in> \<real>; y \<in> Infinitesimal; 0 < x |] ==> y < x"
   7.155  apply (simp add: Infinitesimal_def)
   7.156  apply (rule abs_ge_self [THEN order_le_less_trans], auto)
   7.157  done
   7.158 @@ -917,29 +917,29 @@
   7.159  by (blast intro: Infinitesimal_less_SReal)
   7.160  
   7.161  lemma SReal_not_Infinitesimal:
   7.162 -     "[| 0 < y;  (y::hypreal) \<in> Reals|] ==> y \<notin> Infinitesimal"
   7.163 +     "[| 0 < y;  (y::hypreal) \<in> \<real>|] ==> y \<notin> Infinitesimal"
   7.164  apply (simp add: Infinitesimal_def)
   7.165  apply (auto simp add: abs_if)
   7.166  done
   7.167  
   7.168  lemma SReal_minus_not_Infinitesimal:
   7.169 -     "[| y < 0;  (y::hypreal) \<in> Reals |] ==> y \<notin> Infinitesimal"
   7.170 +     "[| y < 0;  (y::hypreal) \<in> \<real> |] ==> y \<notin> Infinitesimal"
   7.171  apply (subst Infinitesimal_minus_iff [symmetric])
   7.172  apply (rule SReal_not_Infinitesimal, auto)
   7.173  done
   7.174  
   7.175 -lemma SReal_Int_Infinitesimal_zero: "Reals Int Infinitesimal = {0::hypreal}"
   7.176 +lemma SReal_Int_Infinitesimal_zero: "\<real> Int Infinitesimal = {0::hypreal}"
   7.177  apply auto
   7.178  apply (cut_tac x = x and y = 0 in linorder_less_linear)
   7.179  apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
   7.180  done
   7.181  
   7.182  lemma SReal_Infinitesimal_zero:
   7.183 -  "[| (x::hypreal) \<in> Reals; x \<in> Infinitesimal|] ==> x = 0"
   7.184 +  "[| (x::hypreal) \<in> \<real>; x \<in> Infinitesimal|] ==> x = 0"
   7.185  by (cut_tac SReal_Int_Infinitesimal_zero, blast)
   7.186  
   7.187  lemma SReal_HFinite_diff_Infinitesimal:
   7.188 -     "[| (x::hypreal) \<in> Reals; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
   7.189 +     "[| (x::hypreal) \<in> \<real>; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
   7.190  by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD])
   7.191  
   7.192  lemma hypreal_of_real_HFinite_diff_Infinitesimal:
   7.193 @@ -971,7 +971,7 @@
   7.194  done
   7.195  
   7.196  lemma approx_SReal_not_zero:
   7.197 -  "[| (y::hypreal) \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
   7.198 +  "[| (y::hypreal) \<in> \<real>; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
   7.199  apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
   7.200  apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
   7.201  done
   7.202 @@ -996,7 +996,7 @@
   7.203  done
   7.204  
   7.205  lemma Infinitesimal_SReal_divide:
   7.206 -  "[| (x::hypreal) \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
   7.207 +  "[| (x::hypreal) \<in> Infinitesimal; y \<in> \<real> |] ==> x/y \<in> Infinitesimal"
   7.208  apply (simp add: divide_inverse)
   7.209  apply (auto intro!: Infinitesimal_HFinite_mult
   7.210              dest!: Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
   7.211 @@ -1018,7 +1018,7 @@
   7.212  done
   7.213  
   7.214  lemma SReal_approx_iff:
   7.215 -  "[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
   7.216 +  "[|(x::hypreal) \<in> \<real>; y \<in> \<real>|] ==> (x @= y) = (x = y)"
   7.217  apply auto
   7.218  apply (simp add: approx_def)
   7.219  apply (drule (1) Reals_diff)
   7.220 @@ -1060,7 +1060,7 @@
   7.221  by (simp_all add: star_of_approx_iff [symmetric])
   7.222  
   7.223  lemma approx_unique_real:
   7.224 -     "[| (r::hypreal) \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
   7.225 +     "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r @= x; s @= x|] ==> r = s"
   7.226  by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
   7.227  
   7.228  
   7.229 @@ -1069,12 +1069,12 @@
   7.230  subsubsection{*Lifting of the Ub and Lub Properties*}
   7.231  
   7.232  lemma hypreal_of_real_isUb_iff:
   7.233 -      "(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) =
   7.234 +      "(isUb \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) =
   7.235         (isUb (UNIV :: real set) Q Y)"
   7.236  by (simp add: isUb_def setle_def)
   7.237  
   7.238  lemma hypreal_of_real_isLub1:
   7.239 -     "isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)
   7.240 +     "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)
   7.241        ==> isLub (UNIV :: real set) Q Y"
   7.242  apply (simp add: isLub_def leastP_def)
   7.243  apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2]
   7.244 @@ -1083,30 +1083,30 @@
   7.245  
   7.246  lemma hypreal_of_real_isLub2:
   7.247        "isLub (UNIV :: real set) Q Y
   7.248 -       ==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)"
   7.249 +       ==> isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)"
   7.250  apply (auto simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def)
   7.251  by (metis SReal_iff hypreal_of_real_isUb_iff isUbD2a star_of_le)
   7.252  
   7.253  lemma hypreal_of_real_isLub_iff:
   7.254 -     "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) =
   7.255 +     "(isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) =
   7.256        (isLub (UNIV :: real set) Q Y)"
   7.257  by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
   7.258  
   7.259  lemma lemma_isUb_hypreal_of_real:
   7.260 -     "isUb Reals P Y ==> \<exists>Yo. isUb Reals P (hypreal_of_real Yo)"
   7.261 +     "isUb \<real> P Y ==> \<exists>Yo. isUb \<real> P (hypreal_of_real Yo)"
   7.262  by (auto simp add: SReal_iff isUb_def)
   7.263  
   7.264  lemma lemma_isLub_hypreal_of_real:
   7.265 -     "isLub Reals P Y ==> \<exists>Yo. isLub Reals P (hypreal_of_real Yo)"
   7.266 +     "isLub \<real> P Y ==> \<exists>Yo. isLub \<real> P (hypreal_of_real Yo)"
   7.267  by (auto simp add: isLub_def leastP_def isUb_def SReal_iff)
   7.268  
   7.269  lemma lemma_isLub_hypreal_of_real2:
   7.270 -     "\<exists>Yo. isLub Reals P (hypreal_of_real Yo) ==> \<exists>Y. isLub Reals P Y"
   7.271 +     "\<exists>Yo. isLub \<real> P (hypreal_of_real Yo) ==> \<exists>Y. isLub \<real> P Y"
   7.272  by (auto simp add: isLub_def leastP_def isUb_def)
   7.273  
   7.274  lemma SReal_complete:
   7.275 -     "[| P \<subseteq> Reals;  \<exists>x. x \<in> P;  \<exists>Y. isUb Reals P Y |]
   7.276 -      ==> \<exists>t::hypreal. isLub Reals P t"
   7.277 +     "[| P \<subseteq> \<real>;  \<exists>x. x \<in> P;  \<exists>Y. isUb \<real> P Y |]
   7.278 +      ==> \<exists>t::hypreal. isLub \<real> P t"
   7.279  apply (frule SReal_hypreal_of_real_image)
   7.280  apply (auto, drule lemma_isUb_hypreal_of_real)
   7.281  apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2
   7.282 @@ -1116,14 +1116,14 @@
   7.283  (* lemma about lubs *)
   7.284  
   7.285  lemma lemma_st_part_ub:
   7.286 -     "(x::hypreal) \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u"
   7.287 +     "(x::hypreal) \<in> HFinite ==> \<exists>u. isUb \<real> {s. s \<in> \<real> & s < x} u"
   7.288  apply (drule HFiniteD, safe)
   7.289  apply (rule exI, rule isUbI)
   7.290  apply (auto intro: setleI isUbI simp add: abs_less_iff)
   7.291  done
   7.292  
   7.293  lemma lemma_st_part_nonempty:
   7.294 -  "(x::hypreal) \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> Reals & s < x}"
   7.295 +  "(x::hypreal) \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> \<real> & s < x}"
   7.296  apply (drule HFiniteD, safe)
   7.297  apply (drule Reals_minus)
   7.298  apply (rule_tac x = "-t" in exI)
   7.299 @@ -1131,12 +1131,12 @@
   7.300  done
   7.301  
   7.302  lemma lemma_st_part_lub:
   7.303 -     "(x::hypreal) \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t"
   7.304 +     "(x::hypreal) \<in> HFinite ==> \<exists>t. isLub \<real> {s. s \<in> \<real> & s < x} t"
   7.305  by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty Collect_restrict)
   7.306  
   7.307  lemma lemma_st_part_le1:
   7.308 -     "[| (x::hypreal) \<in> HFinite;  isLub Reals {s. s \<in> Reals & s < x} t;
   7.309 -         r \<in> Reals;  0 < r |] ==> x \<le> t + r"
   7.310 +     "[| (x::hypreal) \<in> HFinite;  isLub \<real> {s. s \<in> \<real> & s < x} t;
   7.311 +         r \<in> \<real>;  0 < r |] ==> x \<le> t + r"
   7.312  apply (frule isLubD1a)
   7.313  apply (rule ccontr, drule linorder_not_le [THEN iffD2])
   7.314  apply (drule (1) Reals_add)
   7.315 @@ -1156,8 +1156,8 @@
   7.316  done
   7.317  
   7.318  lemma lemma_st_part_gt_ub:
   7.319 -     "[| (x::hypreal) \<in> HFinite; x < y; y \<in> Reals |]
   7.320 -      ==> isUb Reals {s. s \<in> Reals & s < x} y"
   7.321 +     "[| (x::hypreal) \<in> HFinite; x < y; y \<in> \<real> |]
   7.322 +      ==> isUb \<real> {s. s \<in> \<real> & s < x} y"
   7.323  by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
   7.324  
   7.325  lemma lemma_minus_le_zero: "t \<le> t + -r ==> r \<le> (0::hypreal)"
   7.326 @@ -1167,8 +1167,8 @@
   7.327  
   7.328  lemma lemma_st_part_le2:
   7.329       "[| (x::hypreal) \<in> HFinite;
   7.330 -         isLub Reals {s. s \<in> Reals & s < x} t;
   7.331 -         r \<in> Reals; 0 < r |]
   7.332 +         isLub \<real> {s. s \<in> \<real> & s < x} t;
   7.333 +         r \<in> \<real>; 0 < r |]
   7.334        ==> t + -r \<le> x"
   7.335  apply (frule isLubD1a)
   7.336  apply (rule ccontr, drule linorder_not_le [THEN iffD1])
   7.337 @@ -1181,8 +1181,8 @@
   7.338  
   7.339  lemma lemma_st_part1a:
   7.340       "[| (x::hypreal) \<in> HFinite;
   7.341 -         isLub Reals {s. s \<in> Reals & s < x} t;
   7.342 -         r \<in> Reals; 0 < r |]
   7.343 +         isLub \<real> {s. s \<in> \<real> & s < x} t;
   7.344 +         r \<in> \<real>; 0 < r |]
   7.345        ==> x + -t \<le> r"
   7.346  apply (subgoal_tac "x \<le> t+r")
   7.347  apply (auto intro: lemma_st_part_le1)
   7.348 @@ -1190,8 +1190,8 @@
   7.349  
   7.350  lemma lemma_st_part2a:
   7.351       "[| (x::hypreal) \<in> HFinite;
   7.352 -         isLub Reals {s. s \<in> Reals & s < x} t;
   7.353 -         r \<in> Reals;  0 < r |]
   7.354 +         isLub \<real> {s. s \<in> \<real> & s < x} t;
   7.355 +         r \<in> \<real>;  0 < r |]
   7.356        ==> -(x + -t) \<le> r"
   7.357  apply (subgoal_tac "(t + -r \<le> x)")
   7.358  apply simp
   7.359 @@ -1200,11 +1200,11 @@
   7.360  done
   7.361  
   7.362  lemma lemma_SReal_ub:
   7.363 -     "(x::hypreal) \<in> Reals ==> isUb Reals {s. s \<in> Reals & s < x} x"
   7.364 +     "(x::hypreal) \<in> \<real> ==> isUb \<real> {s. s \<in> \<real> & s < x} x"
   7.365  by (auto intro: isUbI setleI order_less_imp_le)
   7.366  
   7.367  lemma lemma_SReal_lub:
   7.368 -     "(x::hypreal) \<in> Reals ==> isLub Reals {s. s \<in> Reals & s < x} x"
   7.369 +     "(x::hypreal) \<in> \<real> ==> isLub \<real> {s. s \<in> \<real> & s < x} x"
   7.370  apply (auto intro!: isLubI2 lemma_SReal_ub setgeI)
   7.371  apply (frule isUbD2a)
   7.372  apply (rule_tac x = x and y = y in linorder_cases)
   7.373 @@ -1216,8 +1216,8 @@
   7.374  
   7.375  lemma lemma_st_part_not_eq1:
   7.376       "[| (x::hypreal) \<in> HFinite;
   7.377 -         isLub Reals {s. s \<in> Reals & s < x} t;
   7.378 -         r \<in> Reals; 0 < r |]
   7.379 +         isLub \<real> {s. s \<in> \<real> & s < x} t;
   7.380 +         r \<in> \<real>; 0 < r |]
   7.381        ==> x + -t \<noteq> r"
   7.382  apply auto
   7.383  apply (frule isLubD1a [THEN Reals_minus])
   7.384 @@ -1228,8 +1228,8 @@
   7.385  
   7.386  lemma lemma_st_part_not_eq2:
   7.387       "[| (x::hypreal) \<in> HFinite;
   7.388 -         isLub Reals {s. s \<in> Reals & s < x} t;
   7.389 -         r \<in> Reals; 0 < r |]
   7.390 +         isLub \<real> {s. s \<in> \<real> & s < x} t;
   7.391 +         r \<in> \<real>; 0 < r |]
   7.392        ==> -(x + -t) \<noteq> r"
   7.393  apply (auto)
   7.394  apply (frule isLubD1a)
   7.395 @@ -1240,8 +1240,8 @@
   7.396  
   7.397  lemma lemma_st_part_major:
   7.398       "[| (x::hypreal) \<in> HFinite;
   7.399 -         isLub Reals {s. s \<in> Reals & s < x} t;
   7.400 -         r \<in> Reals; 0 < r |]
   7.401 +         isLub \<real> {s. s \<in> \<real> & s < x} t;
   7.402 +         r \<in> \<real>; 0 < r |]
   7.403        ==> abs (x - t) < r"
   7.404  apply (frule lemma_st_part1a)
   7.405  apply (frule_tac [4] lemma_st_part2a, auto)
   7.406 @@ -1250,7 +1250,7 @@
   7.407  done
   7.408  
   7.409  lemma lemma_st_part_major2:
   7.410 -     "[| (x::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t |]
   7.411 +     "[| (x::hypreal) \<in> HFinite; isLub \<real> {s. s \<in> \<real> & s < x} t |]
   7.412        ==> \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r"
   7.413  by (blast dest!: lemma_st_part_major)
   7.414  
   7.415 @@ -1271,7 +1271,7 @@
   7.416  done
   7.417  
   7.418  text{*There is a unique real infinitely close*}
   7.419 -lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> Reals & x @= t"
   7.420 +lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x @= t"
   7.421  apply (drule st_part_Ex, safe)
   7.422  apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
   7.423  apply (auto intro!: approx_unique_real)
   7.424 @@ -1471,7 +1471,7 @@
   7.425  done
   7.426  
   7.427  lemma HInfinite_gt_SReal:
   7.428 -  "[| (x::hypreal) \<in> HInfinite; 0 < x; y \<in> Reals |] ==> y < x"
   7.429 +  "[| (x::hypreal) \<in> HInfinite; 0 < x; y \<in> \<real> |] ==> y < x"
   7.430  by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le)
   7.431  
   7.432  lemma HInfinite_gt_zero_gt_one:
   7.433 @@ -1762,7 +1762,7 @@
   7.434  apply (auto intro: approx_sym)
   7.435  done
   7.436  
   7.437 -lemma st_SReal: "x \<in> HFinite ==> st x \<in> Reals"
   7.438 +lemma st_SReal: "x \<in> HFinite ==> st x \<in> \<real>"
   7.439  apply (simp add: st_def)
   7.440  apply (frule st_part_Ex, safe)
   7.441  apply (rule someI2)
   7.442 @@ -1780,7 +1780,7 @@
   7.443  apply (auto intro: approx_unique_real)
   7.444  done
   7.445  
   7.446 -lemma st_SReal_eq: "x \<in> Reals ==> st x = x"
   7.447 +lemma st_SReal_eq: "x \<in> \<real> ==> st x = x"
   7.448    by (metis approx_refl st_unique) 
   7.449  
   7.450  lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
   7.451 @@ -1793,7 +1793,7 @@
   7.452    assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x @= y"
   7.453    shows "st x = st y"
   7.454  proof -
   7.455 -  have "st x @= x" "st y @= y" "st x \<in> Reals" "st y \<in> Reals"
   7.456 +  have "st x @= x" "st y @= y" "st x \<in> \<real>" "st y \<in> \<real>"
   7.457      by (simp_all add: st_approx_self st_SReal x y)
   7.458    with xy show ?thesis
   7.459      by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
   7.460 @@ -1805,13 +1805,13 @@
   7.461  by (blast intro: approx_st_eq st_eq_approx)
   7.462  
   7.463  lemma st_Infinitesimal_add_SReal:
   7.464 -     "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(x + e) = x"
   7.465 +     "[| x \<in> \<real>; e \<in> Infinitesimal |] ==> st(x + e) = x"
   7.466  apply (erule st_unique)
   7.467  apply (erule Infinitesimal_add_approx_self)
   7.468  done
   7.469  
   7.470  lemma st_Infinitesimal_add_SReal2:
   7.471 -     "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(e + x) = x"
   7.472 +     "[| x \<in> \<real>; e \<in> Infinitesimal |] ==> st(e + x) = x"
   7.473  apply (erule st_unique)
   7.474  apply (erule Infinitesimal_add_approx_self2)
   7.475  done
     8.1 --- a/src/HOL/NSA/NSCA.thy	Mon Aug 31 21:01:21 2015 +0200
     8.2 +++ b/src/HOL/NSA/NSCA.thy	Mon Aug 31 21:28:08 2015 +0200
     8.3 @@ -29,13 +29,13 @@
     8.4  by (drule (1) Standard_diff, simp)
     8.5  
     8.6  lemma SReal_hcmod_hcomplex_of_complex [simp]:
     8.7 -     "hcmod (hcomplex_of_complex r) \<in> Reals"
     8.8 +     "hcmod (hcomplex_of_complex r) \<in> \<real>"
     8.9  by (simp add: Reals_eq_Standard)
    8.10  
    8.11 -lemma SReal_hcmod_numeral [simp]: "hcmod (numeral w ::hcomplex) \<in> Reals"
    8.12 +lemma SReal_hcmod_numeral [simp]: "hcmod (numeral w ::hcomplex) \<in> \<real>"
    8.13  by (simp add: Reals_eq_Standard)
    8.14  
    8.15 -lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals"
    8.16 +lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> \<real>"
    8.17  by (simp add: Reals_eq_Standard)
    8.18  
    8.19  lemma SComplex_divide_numeral:
    8.20 @@ -482,7 +482,7 @@
    8.21  by (simp add: hcomplex_HFinite_iff)
    8.22  
    8.23  lemma SComplex_SReal_hcomplex_of_hypreal:
    8.24 -     "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
    8.25 +     "x \<in> \<real> ==>  hcomplex_of_hypreal x \<in> SComplex"
    8.26  apply (rule Standard_of_hypreal)
    8.27  apply (simp add: Reals_eq_Standard)
    8.28  done
     9.1 --- a/src/HOL/NSA/Star.thy	Mon Aug 31 21:01:21 2015 +0200
     9.2 +++ b/src/HOL/NSA/Star.thy	Mon Aug 31 21:28:08 2015 +0200
     9.3 @@ -53,7 +53,7 @@
     9.4  lemma STAR_star_of_image_subset: "star_of ` A <= *s* A"
     9.5  by auto
     9.6  
     9.7 -lemma STAR_hypreal_of_real_Int: "*s* X Int Reals = hypreal_of_real ` X"
     9.8 +lemma STAR_hypreal_of_real_Int: "*s* X Int \<real> = hypreal_of_real ` X"
     9.9  by (auto simp add: SReal_def)
    9.10  
    9.11  lemma STAR_star_of_Int: "*s* X Int Standard = star_of ` X"
    10.1 --- a/src/HOL/Nat.thy	Mon Aug 31 21:01:21 2015 +0200
    10.2 +++ b/src/HOL/Nat.thy	Mon Aug 31 21:28:08 2015 +0200
    10.3 @@ -1588,11 +1588,8 @@
    10.4  context semiring_1
    10.5  begin
    10.6  
    10.7 -definition Nats  :: "'a set" where
    10.8 -  "Nats = range of_nat"
    10.9 -
   10.10 -notation (xsymbols)
   10.11 -  Nats  ("\<nat>")
   10.12 +definition Nats :: "'a set"  ("\<nat>")
   10.13 +  where "\<nat> = range of_nat"
   10.14  
   10.15  lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
   10.16    by (simp add: Nats_def)
    11.1 --- a/src/HOL/Rat.thy	Mon Aug 31 21:01:21 2015 +0200
    11.2 +++ b/src/HOL/Rat.thy	Mon Aug 31 21:28:08 2015 +0200
    11.3 @@ -808,58 +808,54 @@
    11.4  context field_char_0
    11.5  begin
    11.6  
    11.7 -definition
    11.8 -  Rats  :: "'a set" where
    11.9 -  "Rats = range of_rat"
   11.10 -
   11.11 -notation (xsymbols)
   11.12 -  Rats  ("\<rat>")
   11.13 +definition Rats :: "'a set" ("\<rat>")
   11.14 +  where "\<rat> = range of_rat"
   11.15  
   11.16  end
   11.17  
   11.18 -lemma Rats_of_rat [simp]: "of_rat r \<in> Rats"
   11.19 +lemma Rats_of_rat [simp]: "of_rat r \<in> \<rat>"
   11.20  by (simp add: Rats_def)
   11.21  
   11.22 -lemma Rats_of_int [simp]: "of_int z \<in> Rats"
   11.23 +lemma Rats_of_int [simp]: "of_int z \<in> \<rat>"
   11.24  by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat)
   11.25  
   11.26 -lemma Rats_of_nat [simp]: "of_nat n \<in> Rats"
   11.27 +lemma Rats_of_nat [simp]: "of_nat n \<in> \<rat>"
   11.28  by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat)
   11.29  
   11.30 -lemma Rats_number_of [simp]: "numeral w \<in> Rats"
   11.31 +lemma Rats_number_of [simp]: "numeral w \<in> \<rat>"
   11.32  by (subst of_rat_numeral_eq [symmetric], rule Rats_of_rat)
   11.33  
   11.34 -lemma Rats_0 [simp]: "0 \<in> Rats"
   11.35 +lemma Rats_0 [simp]: "0 \<in> \<rat>"
   11.36  apply (unfold Rats_def)
   11.37  apply (rule range_eqI)
   11.38  apply (rule of_rat_0 [symmetric])
   11.39  done
   11.40  
   11.41 -lemma Rats_1 [simp]: "1 \<in> Rats"
   11.42 +lemma Rats_1 [simp]: "1 \<in> \<rat>"
   11.43  apply (unfold Rats_def)
   11.44  apply (rule range_eqI)
   11.45  apply (rule of_rat_1 [symmetric])
   11.46  done
   11.47  
   11.48 -lemma Rats_add [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a + b \<in> Rats"
   11.49 +lemma Rats_add [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a + b \<in> \<rat>"
   11.50  apply (auto simp add: Rats_def)
   11.51  apply (rule range_eqI)
   11.52  apply (rule of_rat_add [symmetric])
   11.53  done
   11.54  
   11.55 -lemma Rats_minus [simp]: "a \<in> Rats \<Longrightarrow> - a \<in> Rats"
   11.56 +lemma Rats_minus [simp]: "a \<in> \<rat> \<Longrightarrow> - a \<in> \<rat>"
   11.57  apply (auto simp add: Rats_def)
   11.58  apply (rule range_eqI)
   11.59  apply (rule of_rat_minus [symmetric])
   11.60  done
   11.61  
   11.62 -lemma Rats_diff [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a - b \<in> Rats"
   11.63 +lemma Rats_diff [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a - b \<in> \<rat>"
   11.64  apply (auto simp add: Rats_def)
   11.65  apply (rule range_eqI)
   11.66  apply (rule of_rat_diff [symmetric])
   11.67  done
   11.68  
   11.69 -lemma Rats_mult [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a * b \<in> Rats"
   11.70 +lemma Rats_mult [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a * b \<in> \<rat>"
   11.71  apply (auto simp add: Rats_def)
   11.72  apply (rule range_eqI)
   11.73  apply (rule of_rat_mult [symmetric])
   11.74 @@ -867,7 +863,7 @@
   11.75  
   11.76  lemma nonzero_Rats_inverse:
   11.77    fixes a :: "'a::field_char_0"
   11.78 -  shows "\<lbrakk>a \<in> Rats; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Rats"
   11.79 +  shows "\<lbrakk>a \<in> \<rat>; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> \<rat>"
   11.80  apply (auto simp add: Rats_def)
   11.81  apply (rule range_eqI)
   11.82  apply (erule nonzero_of_rat_inverse [symmetric])
   11.83 @@ -875,7 +871,7 @@
   11.84  
   11.85  lemma Rats_inverse [simp]:
   11.86    fixes a :: "'a::{field_char_0, field}"
   11.87 -  shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
   11.88 +  shows "a \<in> \<rat> \<Longrightarrow> inverse a \<in> \<rat>"
   11.89  apply (auto simp add: Rats_def)
   11.90  apply (rule range_eqI)
   11.91  apply (rule of_rat_inverse [symmetric])
   11.92 @@ -883,7 +879,7 @@
   11.93  
   11.94  lemma nonzero_Rats_divide:
   11.95    fixes a b :: "'a::field_char_0"
   11.96 -  shows "\<lbrakk>a \<in> Rats; b \<in> Rats; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
   11.97 +  shows "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> \<rat>"
   11.98  apply (auto simp add: Rats_def)
   11.99  apply (rule range_eqI)
  11.100  apply (erule nonzero_of_rat_divide [symmetric])
  11.101 @@ -891,7 +887,7 @@
  11.102  
  11.103  lemma Rats_divide [simp]:
  11.104    fixes a b :: "'a::{field_char_0, field}"
  11.105 -  shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
  11.106 +  shows "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a / b \<in> \<rat>"
  11.107  apply (auto simp add: Rats_def)
  11.108  apply (rule range_eqI)
  11.109  apply (rule of_rat_divide [symmetric])
  11.110 @@ -899,7 +895,7 @@
  11.111  
  11.112  lemma Rats_power [simp]:
  11.113    fixes a :: "'a::field_char_0"
  11.114 -  shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
  11.115 +  shows "a \<in> \<rat> \<Longrightarrow> a ^ n \<in> \<rat>"
  11.116  apply (auto simp add: Rats_def)
  11.117  apply (rule range_eqI)
  11.118  apply (rule of_rat_power [symmetric])
    12.1 --- a/src/HOL/Real.thy	Mon Aug 31 21:01:21 2015 +0200
    12.2 +++ b/src/HOL/Real.thy	Mon Aug 31 21:28:08 2015 +0200
    12.3 @@ -1163,7 +1163,7 @@
    12.4  lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" 
    12.5  by (insert real_of_int_div2 [of n x], simp)
    12.6  
    12.7 -lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
    12.8 +lemma Ints_real_of_int [simp]: "real (x::int) \<in> \<int>"
    12.9  unfolding real_of_int_def by (rule Ints_of_int)
   12.10  
   12.11  
   12.12 @@ -1300,10 +1300,10 @@
   12.13    apply (simp only: real_of_int_of_nat_eq)
   12.14  done
   12.15  
   12.16 -lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
   12.17 +lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> \<nat>"
   12.18  unfolding real_of_nat_def by (rule of_nat_in_Nats)
   12.19  
   12.20 -lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
   12.21 +lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> \<int>"
   12.22  unfolding real_of_nat_def by (rule Ints_of_nat)
   12.23  
   12.24  subsection \<open>The Archimedean Property of the Reals\<close>
    13.1 --- a/src/HOL/Real_Vector_Spaces.thy	Mon Aug 31 21:01:21 2015 +0200
    13.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Aug 31 21:28:08 2015 +0200
    13.3 @@ -358,55 +358,52 @@
    13.4  
    13.5  subsection \<open>The Set of Real Numbers\<close>
    13.6  
    13.7 -definition Reals :: "'a::real_algebra_1 set" where
    13.8 -  "Reals = range of_real"
    13.9 +definition Reals :: "'a::real_algebra_1 set"  ("\<real>")
   13.10 +  where "\<real> = range of_real"
   13.11  
   13.12 -notation (xsymbols)
   13.13 -  Reals  ("\<real>")
   13.14 -
   13.15 -lemma Reals_of_real [simp]: "of_real r \<in> Reals"
   13.16 +lemma Reals_of_real [simp]: "of_real r \<in> \<real>"
   13.17  by (simp add: Reals_def)
   13.18  
   13.19 -lemma Reals_of_int [simp]: "of_int z \<in> Reals"
   13.20 +lemma Reals_of_int [simp]: "of_int z \<in> \<real>"
   13.21  by (subst of_real_of_int_eq [symmetric], rule Reals_of_real)
   13.22  
   13.23 -lemma Reals_of_nat [simp]: "of_nat n \<in> Reals"
   13.24 +lemma Reals_of_nat [simp]: "of_nat n \<in> \<real>"
   13.25  by (subst of_real_of_nat_eq [symmetric], rule Reals_of_real)
   13.26  
   13.27 -lemma Reals_numeral [simp]: "numeral w \<in> Reals"
   13.28 +lemma Reals_numeral [simp]: "numeral w \<in> \<real>"
   13.29  by (subst of_real_numeral [symmetric], rule Reals_of_real)
   13.30  
   13.31 -lemma Reals_0 [simp]: "0 \<in> Reals"
   13.32 +lemma Reals_0 [simp]: "0 \<in> \<real>"
   13.33  apply (unfold Reals_def)
   13.34  apply (rule range_eqI)
   13.35  apply (rule of_real_0 [symmetric])
   13.36  done
   13.37  
   13.38 -lemma Reals_1 [simp]: "1 \<in> Reals"
   13.39 +lemma Reals_1 [simp]: "1 \<in> \<real>"
   13.40  apply (unfold Reals_def)
   13.41  apply (rule range_eqI)
   13.42  apply (rule of_real_1 [symmetric])
   13.43  done
   13.44  
   13.45 -lemma Reals_add [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a + b \<in> Reals"
   13.46 +lemma Reals_add [simp]: "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a + b \<in> \<real>"
   13.47  apply (auto simp add: Reals_def)
   13.48  apply (rule range_eqI)
   13.49  apply (rule of_real_add [symmetric])
   13.50  done
   13.51  
   13.52 -lemma Reals_minus [simp]: "a \<in> Reals \<Longrightarrow> - a \<in> Reals"
   13.53 +lemma Reals_minus [simp]: "a \<in> \<real> \<Longrightarrow> - a \<in> \<real>"
   13.54  apply (auto simp add: Reals_def)
   13.55  apply (rule range_eqI)
   13.56  apply (rule of_real_minus [symmetric])
   13.57  done
   13.58  
   13.59 -lemma Reals_diff [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a - b \<in> Reals"
   13.60 +lemma Reals_diff [simp]: "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a - b \<in> \<real>"
   13.61  apply (auto simp add: Reals_def)
   13.62  apply (rule range_eqI)
   13.63  apply (rule of_real_diff [symmetric])
   13.64  done
   13.65  
   13.66 -lemma Reals_mult [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a * b \<in> Reals"
   13.67 +lemma Reals_mult [simp]: "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a * b \<in> \<real>"
   13.68  apply (auto simp add: Reals_def)
   13.69  apply (rule range_eqI)
   13.70  apply (rule of_real_mult [symmetric])
   13.71 @@ -414,7 +411,7 @@
   13.72  
   13.73  lemma nonzero_Reals_inverse:
   13.74    fixes a :: "'a::real_div_algebra"
   13.75 -  shows "\<lbrakk>a \<in> Reals; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Reals"
   13.76 +  shows "\<lbrakk>a \<in> \<real>; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> \<real>"
   13.77  apply (auto simp add: Reals_def)
   13.78  apply (rule range_eqI)
   13.79  apply (erule nonzero_of_real_inverse [symmetric])
   13.80 @@ -422,7 +419,7 @@
   13.81  
   13.82  lemma Reals_inverse:
   13.83    fixes a :: "'a::{real_div_algebra, division_ring}"
   13.84 -  shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
   13.85 +  shows "a \<in> \<real> \<Longrightarrow> inverse a \<in> \<real>"
   13.86  apply (auto simp add: Reals_def)
   13.87  apply (rule range_eqI)
   13.88  apply (rule of_real_inverse [symmetric])
   13.89 @@ -435,7 +432,7 @@
   13.90  
   13.91  lemma nonzero_Reals_divide:
   13.92    fixes a b :: "'a::real_field"
   13.93 -  shows "\<lbrakk>a \<in> Reals; b \<in> Reals; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
   13.94 +  shows "\<lbrakk>a \<in> \<real>; b \<in> \<real>; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> \<real>"
   13.95  apply (auto simp add: Reals_def)
   13.96  apply (rule range_eqI)
   13.97  apply (erule nonzero_of_real_divide [symmetric])
   13.98 @@ -443,7 +440,7 @@
   13.99  
  13.100  lemma Reals_divide [simp]:
  13.101    fixes a b :: "'a::{real_field, field}"
  13.102 -  shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
  13.103 +  shows "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a / b \<in> \<real>"
  13.104  apply (auto simp add: Reals_def)
  13.105  apply (rule range_eqI)
  13.106  apply (rule of_real_divide [symmetric])
  13.107 @@ -451,7 +448,7 @@
  13.108  
  13.109  lemma Reals_power [simp]:
  13.110    fixes a :: "'a::{real_algebra_1}"
  13.111 -  shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals"
  13.112 +  shows "a \<in> \<real> \<Longrightarrow> a ^ n \<in> \<real>"
  13.113  apply (auto simp add: Reals_def)
  13.114  apply (rule range_eqI)
  13.115  apply (rule of_real_power [symmetric])
    14.1 --- a/src/HOL/Transcendental.thy	Mon Aug 31 21:01:21 2015 +0200
    14.2 +++ b/src/HOL/Transcendental.thy	Mon Aug 31 21:28:08 2015 +0200
    14.3 @@ -3759,7 +3759,7 @@
    14.4    using sin_cos_squared_add [of x, unfolded assms]
    14.5    by simp
    14.6  
    14.7 -lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
    14.8 +lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> \<int>"
    14.9    by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
   14.10  
   14.11  lemma cos_one_2pi: 
   14.12 @@ -3875,10 +3875,10 @@
   14.13  lemma sin_30: "sin (pi / 6) = 1 / 2"
   14.14    by (simp add: sin_cos_eq cos_60)
   14.15  
   14.16 -lemma cos_integer_2pi: "n \<in> Ints \<Longrightarrow> cos(2*pi * n) = 1"
   14.17 +lemma cos_integer_2pi: "n \<in> \<int> \<Longrightarrow> cos(2*pi * n) = 1"
   14.18    by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
   14.19  
   14.20 -lemma sin_integer_2pi: "n \<in> Ints \<Longrightarrow> sin(2*pi * n) = 0"
   14.21 +lemma sin_integer_2pi: "n \<in> \<int> \<Longrightarrow> sin(2*pi * n) = 0"
   14.22    by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
   14.23  
   14.24  lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"