# HG changeset patch
# User wenzelm
# Date 1441049288 -7200
# Node ID b72a990adfe29d408d7f3efd479e2b4dbe31509f
# Parent  aefe89038dd288e9ca985c3a79b46f351d38fcdb
prefer symbols;

diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Archimedean_Field.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -546,14 +546,14 @@
 lemma frac_lt_1: "frac x < 1"
   by  (simp add: frac_def) linarith
 
-lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> Ints"
+lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> \<int>"
   by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int )
 
 lemma frac_ge_0 [simp]: "frac x \<ge> 0"
   unfolding frac_def
   by linarith
 
-lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> Ints"
+lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> \<int>"
   by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl)
 
 lemma frac_of_int [simp]: "frac (of_int z) = 0"
@@ -582,7 +582,7 @@
 
 lemma frac_unique_iff:
   fixes x :: "'a::floor_ceiling"
-  shows  "(frac x) = a \<longleftrightarrow> x - a \<in> Ints \<and> 0 \<le> a \<and> a < 1"
+  shows  "(frac x) = a \<longleftrightarrow> x - a \<in> \<int> \<and> 0 \<le> a \<and> a < 1"
   apply (auto simp: Ints_def frac_def)
   apply linarith
   apply linarith
@@ -593,7 +593,7 @@
   
 lemma frac_neg:
   fixes x :: "'a::floor_ceiling"
-  shows  "frac (-x) = (if x \<in> Ints then 0 else 1 - frac x)"
+  shows  "frac (-x) = (if x \<in> \<int> then 0 else 1 - frac x)"
   apply (auto simp add: frac_unique_iff)
   apply (simp add: frac_def)
   by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Int.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -623,11 +623,8 @@
 context ring_1
 begin
 
-definition Ints  :: "'a set" where
-  "Ints = range of_int"
-
-notation (xsymbols)
-  Ints  ("\<int>")
+definition Ints :: "'a set"  ("\<int>")
+  where "\<int> = range of_int"
 
 lemma Ints_of_int [simp]: "of_int z \<in> \<int>"
   by (simp add: Ints_def)
@@ -687,7 +684,7 @@
 text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
 
 lemma Ints_double_eq_0_iff:
-  assumes in_Ints: "a \<in> Ints"
+  assumes in_Ints: "a \<in> \<int>"
   shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
 proof -
   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
@@ -706,7 +703,7 @@
 qed
 
 lemma Ints_odd_nonzero:
-  assumes in_Ints: "a \<in> Ints"
+  assumes in_Ints: "a \<in> \<int>"
   shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
 proof -
   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
@@ -720,11 +717,11 @@
   qed
 qed
 
-lemma Nats_numeral [simp]: "numeral w \<in> Nats"
+lemma Nats_numeral [simp]: "numeral w \<in> \<nat>"
   using of_nat_in_Nats [of "numeral w"] by simp
 
 lemma Ints_odd_less_0:
-  assumes in_Ints: "a \<in> Ints"
+  assumes in_Ints: "a \<in> \<int>"
   shows "(1 + a + a < 0) = (a < (0::'a::linordered_idom))"
 proof -
   from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Library/Convex.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -137,7 +137,7 @@
     by (simp only: convex_Int 3 4)
 qed
 
-lemma convex_Reals: "convex Reals"
+lemma convex_Reals: "convex \<real>"
   by (simp add: convex_def scaleR_conv_of_real)
 
 
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -242,9 +242,9 @@
   by (intro open_Collect_less closed_Collect_le closed_Collect_eq isCont_Re
             isCont_Im continuous_ident continuous_const)+
 
-lemma closed_complex_Reals: "closed (Reals :: complex set)"
+lemma closed_complex_Reals: "closed (\<real> :: complex set)"
 proof -
-  have "(Reals :: complex set) = {z. Im z = 0}"
+  have "(\<real> :: complex set) = {z. Im z = 0}"
     by (auto simp: complex_is_Real_iff)
   then show ?thesis
     by (metis closed_halfspace_Im_eq)
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -211,7 +211,7 @@
   by (auto simp: exp_eq abs_mult)
 
 lemma exp_integer_2pi:
-  assumes "n \<in> Ints"
+  assumes "n \<in> \<int>"
   shows "exp((2 * n * pi) * ii) = 1"
 proof -
   have "exp((2 * n * pi) * ii) = exp 0"
@@ -751,15 +751,15 @@
     by blast
 qed
 
-lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z"
+lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
 proof (cases "z=0")
   case True then show ?thesis
     by simp
 next
   case False
-  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)))"
+  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)))"
     by (metis Arg_eq)
-  also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
+  also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
     using False
     by (simp add: zero_le_mult_iff)
   also have "... \<longleftrightarrow> Arg z = 0"
@@ -955,7 +955,7 @@
 corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
   by (simp add: Ln_of_real)
 
-lemma cmod_Ln_Reals [simp]: "z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
+lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
   using Ln_of_real by force
 
 lemma Ln_1: "ln 1 = (0::complex)"
@@ -1565,10 +1565,10 @@
   using lim_Ln_over_power [of 1]
   by simp
 
-lemma Ln_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
+lemma Ln_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
   using Ln_of_real by force
 
-lemma powr_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
+lemma powr_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
   by (simp add: powr_of_real)
 
 lemma lim_ln_over_power:
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/NSA/HyperDef.thy
--- a/src/HOL/NSA/HyperDef.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/NSA/HyperDef.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -103,7 +103,7 @@
     by transfer simp
 qed
 
-lemma Reals_eq_Standard: "(Reals :: hypreal set) = Standard"
+lemma Reals_eq_Standard: "(\<real> :: hypreal set) = Standard"
 by (simp add: Reals_def Standard_def)
 
 
@@ -539,7 +539,7 @@
 by transfer (rule refl)
 
 lemma hyperpow_SReal [simp]:
-     "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> Reals"
+     "(hypreal_of_real r) pow (hypnat_of_nat n) \<in> \<real>"
 by (simp add: Reals_eq_Standard)
 
 lemma hyperpow_zero_HNatInfinite [simp]:
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/NSA/NSA.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -33,7 +33,7 @@
 definition
   st        :: "hypreal => hypreal" where
     --{*the standard part of a hyperreal*}
-  "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
+  "st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r @= x)"
 
 definition
   monad     :: "'a::real_normed_vector star => 'a star set" where
@@ -49,7 +49,7 @@
 notation (HTML output)
   approx  (infixl "\<approx>" 50)
 
-lemma SReal_def: "Reals == {x. \<exists>r. x = hypreal_of_real r}"
+lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}"
 by (simp add: Reals_def image_def)
 
 subsection {* Nonstandard Extension of the Norm Function *}
@@ -176,54 +176,54 @@
 
 subsection{*Closure Laws for the Standard Reals*}
 
-lemma Reals_minus_iff [simp]: "(-x \<in> Reals) = (x \<in> Reals)"
+lemma Reals_minus_iff [simp]: "(-x \<in> \<real>) = (x \<in> \<real>)"
 apply auto
 apply (drule Reals_minus, auto)
 done
 
-lemma Reals_add_cancel: "\<lbrakk>x + y \<in> Reals; y \<in> Reals\<rbrakk> \<Longrightarrow> x \<in> Reals"
+lemma Reals_add_cancel: "\<lbrakk>x + y \<in> \<real>; y \<in> \<real>\<rbrakk> \<Longrightarrow> x \<in> \<real>"
 by (drule (1) Reals_diff, simp)
 
-lemma SReal_hrabs: "(x::hypreal) \<in> Reals ==> abs x \<in> Reals"
+lemma SReal_hrabs: "(x::hypreal) \<in> \<real> ==> abs x \<in> \<real>"
 by (simp add: Reals_eq_Standard)
 
-lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> Reals"
+lemma SReal_hypreal_of_real [simp]: "hypreal_of_real x \<in> \<real>"
 by (simp add: Reals_eq_Standard)
 
-lemma SReal_divide_numeral: "r \<in> Reals ==> r/(numeral w::hypreal) \<in> Reals"
+lemma SReal_divide_numeral: "r \<in> \<real> ==> r/(numeral w::hypreal) \<in> \<real>"
 by simp
 
 text{*epsilon is not in Reals because it is an infinitesimal*}
-lemma SReal_epsilon_not_mem: "epsilon \<notin> Reals"
+lemma SReal_epsilon_not_mem: "epsilon \<notin> \<real>"
 apply (simp add: SReal_def)
 apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym])
 done
 
-lemma SReal_omega_not_mem: "omega \<notin> Reals"
+lemma SReal_omega_not_mem: "omega \<notin> \<real>"
 apply (simp add: SReal_def)
 apply (auto simp add: hypreal_of_real_not_eq_omega [THEN not_sym])
 done
 
-lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> Reals} = (UNIV::real set)"
+lemma SReal_UNIV_real: "{x. hypreal_of_real x \<in> \<real>} = (UNIV::real set)"
 by simp
 
-lemma SReal_iff: "(x \<in> Reals) = (\<exists>y. x = hypreal_of_real y)"
+lemma SReal_iff: "(x \<in> \<real>) = (\<exists>y. x = hypreal_of_real y)"
 by (simp add: SReal_def)
 
-lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = Reals"
+lemma hypreal_of_real_image: "hypreal_of_real `(UNIV::real set) = \<real>"
 by (simp add: Reals_eq_Standard Standard_def)
 
-lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` Reals = UNIV"
+lemma inv_hypreal_of_real_image: "inv hypreal_of_real ` \<real> = UNIV"
 apply (auto simp add: SReal_def)
 apply (rule inj_star_of [THEN inv_f_f, THEN subst], blast)
 done
 
 lemma SReal_hypreal_of_real_image:
-      "[| \<exists>x. x: P; P \<subseteq> Reals |] ==> \<exists>Q. P = hypreal_of_real ` Q"
+      "[| \<exists>x. x: P; P \<subseteq> \<real> |] ==> \<exists>Q. P = hypreal_of_real ` Q"
 by (simp add: SReal_def image_def, blast)
 
 lemma SReal_dense:
-     "[| (x::hypreal) \<in> Reals; y \<in> Reals;  x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
+     "[| (x::hypreal) \<in> \<real>; y \<in> \<real>;  x<y |] ==> \<exists>r \<in> Reals. x<r & r<y"
 apply (auto simp add: SReal_def)
 apply (drule dense, auto)
 done
@@ -231,12 +231,12 @@
 text{*Completeness of Reals, but both lemmas are unused.*}
 
 lemma SReal_sup_lemma:
-     "P \<subseteq> Reals ==> ((\<exists>x \<in> P. y < x) =
+     "P \<subseteq> \<real> ==> ((\<exists>x \<in> P. y < x) =
       (\<exists>X. hypreal_of_real X \<in> P & y < hypreal_of_real X))"
 by (blast dest!: SReal_iff [THEN iffD1])
 
 lemma SReal_sup_lemma2:
-     "[| P \<subseteq> Reals; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
+     "[| P \<subseteq> \<real>; \<exists>x. x \<in> P; \<exists>y \<in> Reals. \<forall>x \<in> P. x < y |]
       ==> (\<exists>X. X \<in> {w. hypreal_of_real w \<in> P}) &
           (\<exists>Y. \<forall>X \<in> {w. hypreal_of_real w \<in> P}. X < Y)"
 apply (rule conjI)
@@ -277,7 +277,7 @@
 apply (blast intro: Reals_add SReal_hypreal_of_real Reals_1)
 done
 
-lemma SReal_subset_HFinite: "(Reals::hypreal set) \<subseteq> HFinite"
+lemma SReal_subset_HFinite: "(\<real>::hypreal set) \<subseteq> HFinite"
 by (auto simp add: SReal_def)
 
 lemma HFiniteD: "x \<in> HFinite ==> \<exists>t \<in> Reals. hnorm x < t"
@@ -850,29 +850,29 @@
 by (blast intro!: approx_mult_HFinite approx_star_of_HFinite HFinite_star_of)
 
 lemma approx_SReal_mult_cancel_zero:
-     "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
+     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a*x @= 0 |] ==> x @= 0"
 apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
 done
 
-lemma approx_mult_SReal1: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> x*a @= 0"
+lemma approx_mult_SReal1: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> x*a @= 0"
 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult1)
 
-lemma approx_mult_SReal2: "[| (a::hypreal) \<in> Reals; x @= 0 |] ==> a*x @= 0"
+lemma approx_mult_SReal2: "[| (a::hypreal) \<in> \<real>; x @= 0 |] ==> a*x @= 0"
 by (auto dest: SReal_subset_HFinite [THEN subsetD] approx_mult2)
 
 lemma approx_mult_SReal_zero_cancel_iff [simp]:
-     "[|(a::hypreal) \<in> Reals; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
+     "[|(a::hypreal) \<in> \<real>; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
 by (blast intro: approx_SReal_mult_cancel_zero approx_mult_SReal2)
 
 lemma approx_SReal_mult_cancel:
-     "[| (a::hypreal) \<in> Reals; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
+     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0; a* w @= a*z |] ==> w @= z"
 apply (drule Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
 apply (auto dest: approx_mult2 simp add: mult.assoc [symmetric])
 done
 
 lemma approx_SReal_mult_cancel_iff1 [simp]:
-     "[| (a::hypreal) \<in> Reals; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
+     "[| (a::hypreal) \<in> \<real>; a \<noteq> 0|] ==> (a* w @= a*z) = (w @= z)"
 by (auto intro!: approx_mult2 SReal_subset_HFinite [THEN subsetD]
          intro: approx_SReal_mult_cancel)
 
@@ -907,7 +907,7 @@
 subsection{* Zero is the Only Infinitesimal that is also a Real*}
 
 lemma Infinitesimal_less_SReal:
-     "[| (x::hypreal) \<in> Reals; y \<in> Infinitesimal; 0 < x |] ==> y < x"
+     "[| (x::hypreal) \<in> \<real>; y \<in> Infinitesimal; 0 < x |] ==> y < x"
 apply (simp add: Infinitesimal_def)
 apply (rule abs_ge_self [THEN order_le_less_trans], auto)
 done
@@ -917,29 +917,29 @@
 by (blast intro: Infinitesimal_less_SReal)
 
 lemma SReal_not_Infinitesimal:
-     "[| 0 < y;  (y::hypreal) \<in> Reals|] ==> y \<notin> Infinitesimal"
+     "[| 0 < y;  (y::hypreal) \<in> \<real>|] ==> y \<notin> Infinitesimal"
 apply (simp add: Infinitesimal_def)
 apply (auto simp add: abs_if)
 done
 
 lemma SReal_minus_not_Infinitesimal:
-     "[| y < 0;  (y::hypreal) \<in> Reals |] ==> y \<notin> Infinitesimal"
+     "[| y < 0;  (y::hypreal) \<in> \<real> |] ==> y \<notin> Infinitesimal"
 apply (subst Infinitesimal_minus_iff [symmetric])
 apply (rule SReal_not_Infinitesimal, auto)
 done
 
-lemma SReal_Int_Infinitesimal_zero: "Reals Int Infinitesimal = {0::hypreal}"
+lemma SReal_Int_Infinitesimal_zero: "\<real> Int Infinitesimal = {0::hypreal}"
 apply auto
 apply (cut_tac x = x and y = 0 in linorder_less_linear)
 apply (blast dest: SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
 done
 
 lemma SReal_Infinitesimal_zero:
-  "[| (x::hypreal) \<in> Reals; x \<in> Infinitesimal|] ==> x = 0"
+  "[| (x::hypreal) \<in> \<real>; x \<in> Infinitesimal|] ==> x = 0"
 by (cut_tac SReal_Int_Infinitesimal_zero, blast)
 
 lemma SReal_HFinite_diff_Infinitesimal:
-     "[| (x::hypreal) \<in> Reals; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
+     "[| (x::hypreal) \<in> \<real>; x \<noteq> 0 |] ==> x \<in> HFinite - Infinitesimal"
 by (auto dest: SReal_Infinitesimal_zero SReal_subset_HFinite [THEN subsetD])
 
 lemma hypreal_of_real_HFinite_diff_Infinitesimal:
@@ -971,7 +971,7 @@
 done
 
 lemma approx_SReal_not_zero:
-  "[| (y::hypreal) \<in> Reals; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
+  "[| (y::hypreal) \<in> \<real>; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
 apply (cut_tac x = 0 and y = y in linorder_less_linear, simp)
 apply (blast dest: approx_sym [THEN mem_infmal_iff [THEN iffD2]] SReal_not_Infinitesimal SReal_minus_not_Infinitesimal)
 done
@@ -996,7 +996,7 @@
 done
 
 lemma Infinitesimal_SReal_divide:
-  "[| (x::hypreal) \<in> Infinitesimal; y \<in> Reals |] ==> x/y \<in> Infinitesimal"
+  "[| (x::hypreal) \<in> Infinitesimal; y \<in> \<real> |] ==> x/y \<in> Infinitesimal"
 apply (simp add: divide_inverse)
 apply (auto intro!: Infinitesimal_HFinite_mult
             dest!: Reals_inverse [THEN SReal_subset_HFinite [THEN subsetD]])
@@ -1018,7 +1018,7 @@
 done
 
 lemma SReal_approx_iff:
-  "[|(x::hypreal) \<in> Reals; y \<in> Reals|] ==> (x @= y) = (x = y)"
+  "[|(x::hypreal) \<in> \<real>; y \<in> \<real>|] ==> (x @= y) = (x = y)"
 apply auto
 apply (simp add: approx_def)
 apply (drule (1) Reals_diff)
@@ -1060,7 +1060,7 @@
 by (simp_all add: star_of_approx_iff [symmetric])
 
 lemma approx_unique_real:
-     "[| (r::hypreal) \<in> Reals; s \<in> Reals; r @= x; s @= x|] ==> r = s"
+     "[| (r::hypreal) \<in> \<real>; s \<in> \<real>; r @= x; s @= x|] ==> r = s"
 by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
 
 
@@ -1069,12 +1069,12 @@
 subsubsection{*Lifting of the Ub and Lub Properties*}
 
 lemma hypreal_of_real_isUb_iff:
-      "(isUb (Reals) (hypreal_of_real ` Q) (hypreal_of_real Y)) =
+      "(isUb \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) =
        (isUb (UNIV :: real set) Q Y)"
 by (simp add: isUb_def setle_def)
 
 lemma hypreal_of_real_isLub1:
-     "isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)
+     "isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)
       ==> isLub (UNIV :: real set) Q Y"
 apply (simp add: isLub_def leastP_def)
 apply (auto intro: hypreal_of_real_isUb_iff [THEN iffD2]
@@ -1083,30 +1083,30 @@
 
 lemma hypreal_of_real_isLub2:
       "isLub (UNIV :: real set) Q Y
-       ==> isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)"
+       ==> isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)"
 apply (auto simp add: isLub_def leastP_def hypreal_of_real_isUb_iff setge_def)
 by (metis SReal_iff hypreal_of_real_isUb_iff isUbD2a star_of_le)
 
 lemma hypreal_of_real_isLub_iff:
-     "(isLub Reals (hypreal_of_real ` Q) (hypreal_of_real Y)) =
+     "(isLub \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) =
       (isLub (UNIV :: real set) Q Y)"
 by (blast intro: hypreal_of_real_isLub1 hypreal_of_real_isLub2)
 
 lemma lemma_isUb_hypreal_of_real:
-     "isUb Reals P Y ==> \<exists>Yo. isUb Reals P (hypreal_of_real Yo)"
+     "isUb \<real> P Y ==> \<exists>Yo. isUb \<real> P (hypreal_of_real Yo)"
 by (auto simp add: SReal_iff isUb_def)
 
 lemma lemma_isLub_hypreal_of_real:
-     "isLub Reals P Y ==> \<exists>Yo. isLub Reals P (hypreal_of_real Yo)"
+     "isLub \<real> P Y ==> \<exists>Yo. isLub \<real> P (hypreal_of_real Yo)"
 by (auto simp add: isLub_def leastP_def isUb_def SReal_iff)
 
 lemma lemma_isLub_hypreal_of_real2:
-     "\<exists>Yo. isLub Reals P (hypreal_of_real Yo) ==> \<exists>Y. isLub Reals P Y"
+     "\<exists>Yo. isLub \<real> P (hypreal_of_real Yo) ==> \<exists>Y. isLub \<real> P Y"
 by (auto simp add: isLub_def leastP_def isUb_def)
 
 lemma SReal_complete:
-     "[| P \<subseteq> Reals;  \<exists>x. x \<in> P;  \<exists>Y. isUb Reals P Y |]
-      ==> \<exists>t::hypreal. isLub Reals P t"
+     "[| P \<subseteq> \<real>;  \<exists>x. x \<in> P;  \<exists>Y. isUb \<real> P Y |]
+      ==> \<exists>t::hypreal. isLub \<real> P t"
 apply (frule SReal_hypreal_of_real_image)
 apply (auto, drule lemma_isUb_hypreal_of_real)
 apply (auto intro!: reals_complete lemma_isLub_hypreal_of_real2
@@ -1116,14 +1116,14 @@
 (* lemma about lubs *)
 
 lemma lemma_st_part_ub:
-     "(x::hypreal) \<in> HFinite ==> \<exists>u. isUb Reals {s. s \<in> Reals & s < x} u"
+     "(x::hypreal) \<in> HFinite ==> \<exists>u. isUb \<real> {s. s \<in> \<real> & s < x} u"
 apply (drule HFiniteD, safe)
 apply (rule exI, rule isUbI)
 apply (auto intro: setleI isUbI simp add: abs_less_iff)
 done
 
 lemma lemma_st_part_nonempty:
-  "(x::hypreal) \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> Reals & s < x}"
+  "(x::hypreal) \<in> HFinite ==> \<exists>y. y \<in> {s. s \<in> \<real> & s < x}"
 apply (drule HFiniteD, safe)
 apply (drule Reals_minus)
 apply (rule_tac x = "-t" in exI)
@@ -1131,12 +1131,12 @@
 done
 
 lemma lemma_st_part_lub:
-     "(x::hypreal) \<in> HFinite ==> \<exists>t. isLub Reals {s. s \<in> Reals & s < x} t"
+     "(x::hypreal) \<in> HFinite ==> \<exists>t. isLub \<real> {s. s \<in> \<real> & s < x} t"
 by (blast intro!: SReal_complete lemma_st_part_ub lemma_st_part_nonempty Collect_restrict)
 
 lemma lemma_st_part_le1:
-     "[| (x::hypreal) \<in> HFinite;  isLub Reals {s. s \<in> Reals & s < x} t;
-         r \<in> Reals;  0 < r |] ==> x \<le> t + r"
+     "[| (x::hypreal) \<in> HFinite;  isLub \<real> {s. s \<in> \<real> & s < x} t;
+         r \<in> \<real>;  0 < r |] ==> x \<le> t + r"
 apply (frule isLubD1a)
 apply (rule ccontr, drule linorder_not_le [THEN iffD2])
 apply (drule (1) Reals_add)
@@ -1156,8 +1156,8 @@
 done
 
 lemma lemma_st_part_gt_ub:
-     "[| (x::hypreal) \<in> HFinite; x < y; y \<in> Reals |]
-      ==> isUb Reals {s. s \<in> Reals & s < x} y"
+     "[| (x::hypreal) \<in> HFinite; x < y; y \<in> \<real> |]
+      ==> isUb \<real> {s. s \<in> \<real> & s < x} y"
 by (auto dest: order_less_trans intro: order_less_imp_le intro!: isUbI setleI)
 
 lemma lemma_minus_le_zero: "t \<le> t + -r ==> r \<le> (0::hypreal)"
@@ -1167,8 +1167,8 @@
 
 lemma lemma_st_part_le2:
      "[| (x::hypreal) \<in> HFinite;
-         isLub Reals {s. s \<in> Reals & s < x} t;
-         r \<in> Reals; 0 < r |]
+         isLub \<real> {s. s \<in> \<real> & s < x} t;
+         r \<in> \<real>; 0 < r |]
       ==> t + -r \<le> x"
 apply (frule isLubD1a)
 apply (rule ccontr, drule linorder_not_le [THEN iffD1])
@@ -1181,8 +1181,8 @@
 
 lemma lemma_st_part1a:
      "[| (x::hypreal) \<in> HFinite;
-         isLub Reals {s. s \<in> Reals & s < x} t;
-         r \<in> Reals; 0 < r |]
+         isLub \<real> {s. s \<in> \<real> & s < x} t;
+         r \<in> \<real>; 0 < r |]
       ==> x + -t \<le> r"
 apply (subgoal_tac "x \<le> t+r")
 apply (auto intro: lemma_st_part_le1)
@@ -1190,8 +1190,8 @@
 
 lemma lemma_st_part2a:
      "[| (x::hypreal) \<in> HFinite;
-         isLub Reals {s. s \<in> Reals & s < x} t;
-         r \<in> Reals;  0 < r |]
+         isLub \<real> {s. s \<in> \<real> & s < x} t;
+         r \<in> \<real>;  0 < r |]
       ==> -(x + -t) \<le> r"
 apply (subgoal_tac "(t + -r \<le> x)")
 apply simp
@@ -1200,11 +1200,11 @@
 done
 
 lemma lemma_SReal_ub:
-     "(x::hypreal) \<in> Reals ==> isUb Reals {s. s \<in> Reals & s < x} x"
+     "(x::hypreal) \<in> \<real> ==> isUb \<real> {s. s \<in> \<real> & s < x} x"
 by (auto intro: isUbI setleI order_less_imp_le)
 
 lemma lemma_SReal_lub:
-     "(x::hypreal) \<in> Reals ==> isLub Reals {s. s \<in> Reals & s < x} x"
+     "(x::hypreal) \<in> \<real> ==> isLub \<real> {s. s \<in> \<real> & s < x} x"
 apply (auto intro!: isLubI2 lemma_SReal_ub setgeI)
 apply (frule isUbD2a)
 apply (rule_tac x = x and y = y in linorder_cases)
@@ -1216,8 +1216,8 @@
 
 lemma lemma_st_part_not_eq1:
      "[| (x::hypreal) \<in> HFinite;
-         isLub Reals {s. s \<in> Reals & s < x} t;
-         r \<in> Reals; 0 < r |]
+         isLub \<real> {s. s \<in> \<real> & s < x} t;
+         r \<in> \<real>; 0 < r |]
       ==> x + -t \<noteq> r"
 apply auto
 apply (frule isLubD1a [THEN Reals_minus])
@@ -1228,8 +1228,8 @@
 
 lemma lemma_st_part_not_eq2:
      "[| (x::hypreal) \<in> HFinite;
-         isLub Reals {s. s \<in> Reals & s < x} t;
-         r \<in> Reals; 0 < r |]
+         isLub \<real> {s. s \<in> \<real> & s < x} t;
+         r \<in> \<real>; 0 < r |]
       ==> -(x + -t) \<noteq> r"
 apply (auto)
 apply (frule isLubD1a)
@@ -1240,8 +1240,8 @@
 
 lemma lemma_st_part_major:
      "[| (x::hypreal) \<in> HFinite;
-         isLub Reals {s. s \<in> Reals & s < x} t;
-         r \<in> Reals; 0 < r |]
+         isLub \<real> {s. s \<in> \<real> & s < x} t;
+         r \<in> \<real>; 0 < r |]
       ==> abs (x - t) < r"
 apply (frule lemma_st_part1a)
 apply (frule_tac [4] lemma_st_part2a, auto)
@@ -1250,7 +1250,7 @@
 done
 
 lemma lemma_st_part_major2:
-     "[| (x::hypreal) \<in> HFinite; isLub Reals {s. s \<in> Reals & s < x} t |]
+     "[| (x::hypreal) \<in> HFinite; isLub \<real> {s. s \<in> \<real> & s < x} t |]
       ==> \<forall>r \<in> Reals. 0 < r --> abs (x - t) < r"
 by (blast dest!: lemma_st_part_major)
 
@@ -1271,7 +1271,7 @@
 done
 
 text{*There is a unique real infinitely close*}
-lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> Reals & x @= t"
+lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x @= t"
 apply (drule st_part_Ex, safe)
 apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
 apply (auto intro!: approx_unique_real)
@@ -1471,7 +1471,7 @@
 done
 
 lemma HInfinite_gt_SReal:
-  "[| (x::hypreal) \<in> HInfinite; 0 < x; y \<in> Reals |] ==> y < x"
+  "[| (x::hypreal) \<in> HInfinite; 0 < x; y \<in> \<real> |] ==> y < x"
 by (auto dest!: bspec simp add: HInfinite_def abs_if order_less_imp_le)
 
 lemma HInfinite_gt_zero_gt_one:
@@ -1762,7 +1762,7 @@
 apply (auto intro: approx_sym)
 done
 
-lemma st_SReal: "x \<in> HFinite ==> st x \<in> Reals"
+lemma st_SReal: "x \<in> HFinite ==> st x \<in> \<real>"
 apply (simp add: st_def)
 apply (frule st_part_Ex, safe)
 apply (rule someI2)
@@ -1780,7 +1780,7 @@
 apply (auto intro: approx_unique_real)
 done
 
-lemma st_SReal_eq: "x \<in> Reals ==> st x = x"
+lemma st_SReal_eq: "x \<in> \<real> ==> st x = x"
   by (metis approx_refl st_unique) 
 
 lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
@@ -1793,7 +1793,7 @@
   assumes x: "x \<in> HFinite" and y: "y \<in> HFinite" and xy: "x @= y"
   shows "st x = st y"
 proof -
-  have "st x @= x" "st y @= y" "st x \<in> Reals" "st y \<in> Reals"
+  have "st x @= x" "st y @= y" "st x \<in> \<real>" "st y \<in> \<real>"
     by (simp_all add: st_approx_self st_SReal x y)
   with xy show ?thesis
     by (fast elim: approx_trans approx_trans2 SReal_approx_iff [THEN iffD1])
@@ -1805,13 +1805,13 @@
 by (blast intro: approx_st_eq st_eq_approx)
 
 lemma st_Infinitesimal_add_SReal:
-     "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(x + e) = x"
+     "[| x \<in> \<real>; e \<in> Infinitesimal |] ==> st(x + e) = x"
 apply (erule st_unique)
 apply (erule Infinitesimal_add_approx_self)
 done
 
 lemma st_Infinitesimal_add_SReal2:
-     "[| x \<in> Reals; e \<in> Infinitesimal |] ==> st(e + x) = x"
+     "[| x \<in> \<real>; e \<in> Infinitesimal |] ==> st(e + x) = x"
 apply (erule st_unique)
 apply (erule Infinitesimal_add_approx_self2)
 done
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/NSA/NSCA.thy
--- a/src/HOL/NSA/NSCA.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/NSA/NSCA.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -29,13 +29,13 @@
 by (drule (1) Standard_diff, simp)
 
 lemma SReal_hcmod_hcomplex_of_complex [simp]:
-     "hcmod (hcomplex_of_complex r) \<in> Reals"
+     "hcmod (hcomplex_of_complex r) \<in> \<real>"
 by (simp add: Reals_eq_Standard)
 
-lemma SReal_hcmod_numeral [simp]: "hcmod (numeral w ::hcomplex) \<in> Reals"
+lemma SReal_hcmod_numeral [simp]: "hcmod (numeral w ::hcomplex) \<in> \<real>"
 by (simp add: Reals_eq_Standard)
 
-lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> Reals"
+lemma SReal_hcmod_SComplex: "x \<in> SComplex ==> hcmod x \<in> \<real>"
 by (simp add: Reals_eq_Standard)
 
 lemma SComplex_divide_numeral:
@@ -482,7 +482,7 @@
 by (simp add: hcomplex_HFinite_iff)
 
 lemma SComplex_SReal_hcomplex_of_hypreal:
-     "x \<in> Reals ==>  hcomplex_of_hypreal x \<in> SComplex"
+     "x \<in> \<real> ==>  hcomplex_of_hypreal x \<in> SComplex"
 apply (rule Standard_of_hypreal)
 apply (simp add: Reals_eq_Standard)
 done
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/NSA/Star.thy
--- a/src/HOL/NSA/Star.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/NSA/Star.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -53,7 +53,7 @@
 lemma STAR_star_of_image_subset: "star_of ` A <= *s* A"
 by auto
 
-lemma STAR_hypreal_of_real_Int: "*s* X Int Reals = hypreal_of_real ` X"
+lemma STAR_hypreal_of_real_Int: "*s* X Int \<real> = hypreal_of_real ` X"
 by (auto simp add: SReal_def)
 
 lemma STAR_star_of_Int: "*s* X Int Standard = star_of ` X"
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Nat.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -1588,11 +1588,8 @@
 context semiring_1
 begin
 
-definition Nats  :: "'a set" where
-  "Nats = range of_nat"
-
-notation (xsymbols)
-  Nats  ("\<nat>")
+definition Nats :: "'a set"  ("\<nat>")
+  where "\<nat> = range of_nat"
 
 lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
   by (simp add: Nats_def)
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Rat.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -808,58 +808,54 @@
 context field_char_0
 begin
 
-definition
-  Rats  :: "'a set" where
-  "Rats = range of_rat"
-
-notation (xsymbols)
-  Rats  ("\<rat>")
+definition Rats :: "'a set" ("\<rat>")
+  where "\<rat> = range of_rat"
 
 end
 
-lemma Rats_of_rat [simp]: "of_rat r \<in> Rats"
+lemma Rats_of_rat [simp]: "of_rat r \<in> \<rat>"
 by (simp add: Rats_def)
 
-lemma Rats_of_int [simp]: "of_int z \<in> Rats"
+lemma Rats_of_int [simp]: "of_int z \<in> \<rat>"
 by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat)
 
-lemma Rats_of_nat [simp]: "of_nat n \<in> Rats"
+lemma Rats_of_nat [simp]: "of_nat n \<in> \<rat>"
 by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat)
 
-lemma Rats_number_of [simp]: "numeral w \<in> Rats"
+lemma Rats_number_of [simp]: "numeral w \<in> \<rat>"
 by (subst of_rat_numeral_eq [symmetric], rule Rats_of_rat)
 
-lemma Rats_0 [simp]: "0 \<in> Rats"
+lemma Rats_0 [simp]: "0 \<in> \<rat>"
 apply (unfold Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_0 [symmetric])
 done
 
-lemma Rats_1 [simp]: "1 \<in> Rats"
+lemma Rats_1 [simp]: "1 \<in> \<rat>"
 apply (unfold Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_1 [symmetric])
 done
 
-lemma Rats_add [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a + b \<in> Rats"
+lemma Rats_add [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a + b \<in> \<rat>"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_add [symmetric])
 done
 
-lemma Rats_minus [simp]: "a \<in> Rats \<Longrightarrow> - a \<in> Rats"
+lemma Rats_minus [simp]: "a \<in> \<rat> \<Longrightarrow> - a \<in> \<rat>"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_minus [symmetric])
 done
 
-lemma Rats_diff [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a - b \<in> Rats"
+lemma Rats_diff [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a - b \<in> \<rat>"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_diff [symmetric])
 done
 
-lemma Rats_mult [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a * b \<in> Rats"
+lemma Rats_mult [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a * b \<in> \<rat>"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_mult [symmetric])
@@ -867,7 +863,7 @@
 
 lemma nonzero_Rats_inverse:
   fixes a :: "'a::field_char_0"
-  shows "\<lbrakk>a \<in> Rats; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Rats"
+  shows "\<lbrakk>a \<in> \<rat>; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> \<rat>"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (erule nonzero_of_rat_inverse [symmetric])
@@ -875,7 +871,7 @@
 
 lemma Rats_inverse [simp]:
   fixes a :: "'a::{field_char_0, field}"
-  shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
+  shows "a \<in> \<rat> \<Longrightarrow> inverse a \<in> \<rat>"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_inverse [symmetric])
@@ -883,7 +879,7 @@
 
 lemma nonzero_Rats_divide:
   fixes a b :: "'a::field_char_0"
-  shows "\<lbrakk>a \<in> Rats; b \<in> Rats; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
+  shows "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> \<rat>"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (erule nonzero_of_rat_divide [symmetric])
@@ -891,7 +887,7 @@
 
 lemma Rats_divide [simp]:
   fixes a b :: "'a::{field_char_0, field}"
-  shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
+  shows "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a / b \<in> \<rat>"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_divide [symmetric])
@@ -899,7 +895,7 @@
 
 lemma Rats_power [simp]:
   fixes a :: "'a::field_char_0"
-  shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
+  shows "a \<in> \<rat> \<Longrightarrow> a ^ n \<in> \<rat>"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_power [symmetric])
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Real.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -1163,7 +1163,7 @@
 lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" 
 by (insert real_of_int_div2 [of n x], simp)
 
-lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
+lemma Ints_real_of_int [simp]: "real (x::int) \<in> \<int>"
 unfolding real_of_int_def by (rule Ints_of_int)
 
 
@@ -1300,10 +1300,10 @@
   apply (simp only: real_of_int_of_nat_eq)
 done
 
-lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
+lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> \<nat>"
 unfolding real_of_nat_def by (rule of_nat_in_Nats)
 
-lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
+lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> \<int>"
 unfolding real_of_nat_def by (rule Ints_of_nat)
 
 subsection \<open>The Archimedean Property of the Reals\<close>
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -358,55 +358,52 @@
 
 subsection \<open>The Set of Real Numbers\<close>
 
-definition Reals :: "'a::real_algebra_1 set" where
-  "Reals = range of_real"
+definition Reals :: "'a::real_algebra_1 set"  ("\<real>")
+  where "\<real> = range of_real"
 
-notation (xsymbols)
-  Reals  ("\<real>")
-
-lemma Reals_of_real [simp]: "of_real r \<in> Reals"
+lemma Reals_of_real [simp]: "of_real r \<in> \<real>"
 by (simp add: Reals_def)
 
-lemma Reals_of_int [simp]: "of_int z \<in> Reals"
+lemma Reals_of_int [simp]: "of_int z \<in> \<real>"
 by (subst of_real_of_int_eq [symmetric], rule Reals_of_real)
 
-lemma Reals_of_nat [simp]: "of_nat n \<in> Reals"
+lemma Reals_of_nat [simp]: "of_nat n \<in> \<real>"
 by (subst of_real_of_nat_eq [symmetric], rule Reals_of_real)
 
-lemma Reals_numeral [simp]: "numeral w \<in> Reals"
+lemma Reals_numeral [simp]: "numeral w \<in> \<real>"
 by (subst of_real_numeral [symmetric], rule Reals_of_real)
 
-lemma Reals_0 [simp]: "0 \<in> Reals"
+lemma Reals_0 [simp]: "0 \<in> \<real>"
 apply (unfold Reals_def)
 apply (rule range_eqI)
 apply (rule of_real_0 [symmetric])
 done
 
-lemma Reals_1 [simp]: "1 \<in> Reals"
+lemma Reals_1 [simp]: "1 \<in> \<real>"
 apply (unfold Reals_def)
 apply (rule range_eqI)
 apply (rule of_real_1 [symmetric])
 done
 
-lemma Reals_add [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a + b \<in> Reals"
+lemma Reals_add [simp]: "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a + b \<in> \<real>"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
 apply (rule of_real_add [symmetric])
 done
 
-lemma Reals_minus [simp]: "a \<in> Reals \<Longrightarrow> - a \<in> Reals"
+lemma Reals_minus [simp]: "a \<in> \<real> \<Longrightarrow> - a \<in> \<real>"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
 apply (rule of_real_minus [symmetric])
 done
 
-lemma Reals_diff [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a - b \<in> Reals"
+lemma Reals_diff [simp]: "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a - b \<in> \<real>"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
 apply (rule of_real_diff [symmetric])
 done
 
-lemma Reals_mult [simp]: "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a * b \<in> Reals"
+lemma Reals_mult [simp]: "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a * b \<in> \<real>"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
 apply (rule of_real_mult [symmetric])
@@ -414,7 +411,7 @@
 
 lemma nonzero_Reals_inverse:
   fixes a :: "'a::real_div_algebra"
-  shows "\<lbrakk>a \<in> Reals; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Reals"
+  shows "\<lbrakk>a \<in> \<real>; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> \<real>"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
 apply (erule nonzero_of_real_inverse [symmetric])
@@ -422,7 +419,7 @@
 
 lemma Reals_inverse:
   fixes a :: "'a::{real_div_algebra, division_ring}"
-  shows "a \<in> Reals \<Longrightarrow> inverse a \<in> Reals"
+  shows "a \<in> \<real> \<Longrightarrow> inverse a \<in> \<real>"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
 apply (rule of_real_inverse [symmetric])
@@ -435,7 +432,7 @@
 
 lemma nonzero_Reals_divide:
   fixes a b :: "'a::real_field"
-  shows "\<lbrakk>a \<in> Reals; b \<in> Reals; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
+  shows "\<lbrakk>a \<in> \<real>; b \<in> \<real>; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> \<real>"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
 apply (erule nonzero_of_real_divide [symmetric])
@@ -443,7 +440,7 @@
 
 lemma Reals_divide [simp]:
   fixes a b :: "'a::{real_field, field}"
-  shows "\<lbrakk>a \<in> Reals; b \<in> Reals\<rbrakk> \<Longrightarrow> a / b \<in> Reals"
+  shows "\<lbrakk>a \<in> \<real>; b \<in> \<real>\<rbrakk> \<Longrightarrow> a / b \<in> \<real>"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
 apply (rule of_real_divide [symmetric])
@@ -451,7 +448,7 @@
 
 lemma Reals_power [simp]:
   fixes a :: "'a::{real_algebra_1}"
-  shows "a \<in> Reals \<Longrightarrow> a ^ n \<in> Reals"
+  shows "a \<in> \<real> \<Longrightarrow> a ^ n \<in> \<real>"
 apply (auto simp add: Reals_def)
 apply (rule range_eqI)
 apply (rule of_real_power [symmetric])
diff -r aefe89038dd2 -r b72a990adfe2 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Aug 31 21:01:21 2015 +0200
+++ b/src/HOL/Transcendental.thy	Mon Aug 31 21:28:08 2015 +0200
@@ -3759,7 +3759,7 @@
   using sin_cos_squared_add [of x, unfolded assms]
   by simp
 
-lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> Ints"
+lemma sin_times_pi_eq_0: "sin(x * pi) = 0 \<longleftrightarrow> x \<in> \<int>"
   by (simp add: sin_zero_iff_int2) (metis Ints_cases Ints_real_of_int real_of_int_def)
 
 lemma cos_one_2pi: 
@@ -3875,10 +3875,10 @@
 lemma sin_30: "sin (pi / 6) = 1 / 2"
   by (simp add: sin_cos_eq cos_60)
 
-lemma cos_integer_2pi: "n \<in> Ints \<Longrightarrow> cos(2*pi * n) = 1"
+lemma cos_integer_2pi: "n \<in> \<int> \<Longrightarrow> cos(2*pi * n) = 1"
   by (metis Ints_cases cos_one_2pi_int mult.assoc mult.commute real_of_int_def)
 
-lemma sin_integer_2pi: "n \<in> Ints \<Longrightarrow> sin(2*pi * n) = 0"
+lemma sin_integer_2pi: "n \<in> \<int> \<Longrightarrow> sin(2*pi * n) = 0"
   by (metis sin_two_pi Ints_mult mult.assoc mult.commute sin_times_pi_eq_0)
 
 lemma cos_int_2npi [simp]: "cos (2 * real (n::int) * pi) = 1"