isabelle update_cartouches -c -t;
authorwenzelm
Wed Dec 30 11:37:29 2015 +0100 (2015-12-30)
changeset 61975b4b11391c676
parent 61974 5b067c681989
child 61976 3a27957ac658
isabelle update_cartouches -c -t;
src/HOL/GCD.thy
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Discrete.thy
src/HOL/Library/Function_Growth.thy
src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Operator_Norm.thy
src/HOL/NSA/CLim.thy
src/HOL/NSA/CStar.thy
src/HOL/NSA/Examples/NSPrimes.thy
src/HOL/NSA/Free_Ultrafilter.thy
src/HOL/NSA/HDeriv.thy
src/HOL/NSA/HLim.thy
src/HOL/NSA/HLog.thy
src/HOL/NSA/HSEQ.thy
src/HOL/NSA/HSeries.thy
src/HOL/NSA/HTranscendental.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/HyperNat.thy
src/HOL/NSA/NSA.thy
src/HOL/NSA/NSCA.thy
src/HOL/NSA/NSComplex.thy
src/HOL/NSA/NatStar.thy
src/HOL/NSA/Star.thy
src/HOL/NSA/StarDef.thy
     1.1 --- a/src/HOL/GCD.thy	Wed Dec 30 11:32:56 2015 +0100
     1.2 +++ b/src/HOL/GCD.thy	Wed Dec 30 11:37:29 2015 +0100
     1.3 @@ -2232,6 +2232,6 @@
     1.4    \<rightharpoonup> (OCaml) "Big'_int.gcd'_big'_int"
     1.5    and (Haskell) "Prelude.gcd"
     1.6    and (Scala) "_.gcd'((_)')"
     1.7 -  -- \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
     1.8 +  \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
     1.9  
    1.10  end
     2.1 --- a/src/HOL/Library/ContNotDenum.thy	Wed Dec 30 11:32:56 2015 +0100
     2.2 +++ b/src/HOL/Library/ContNotDenum.thy	Wed Dec 30 11:37:29 2015 +0100
     2.3 @@ -148,8 +148,8 @@
     2.4    assumes "a < b" and "countable A"
     2.5    shows "\<exists>x\<in>{a<..<b}. x \<notin> A"
     2.6  proof -
     2.7 -  from `countable A` have "countable (A \<inter> {a<..<b})" by auto
     2.8 -  moreover with `a < b` have "\<not> countable {a<..<b}" 
     2.9 +  from \<open>countable A\<close> have "countable (A \<inter> {a<..<b})" by auto
    2.10 +  moreover with \<open>a < b\<close> have "\<not> countable {a<..<b}" 
    2.11      by (simp add: uncountable_open_interval)
    2.12    ultimately have "A \<inter> {a<..<b} \<noteq> {a<..<b}" by auto
    2.13    hence "A \<inter> {a<..<b} \<subset> {a<..<b}" 
     3.1 --- a/src/HOL/Library/Discrete.thy	Wed Dec 30 11:32:56 2015 +0100
     3.2 +++ b/src/HOL/Library/Discrete.thy	Wed Dec 30 11:37:29 2015 +0100
     3.3 @@ -20,7 +20,7 @@
     3.4    assumes one: "P 1"
     3.5    assumes double: "\<And>n. n \<ge> 2 \<Longrightarrow> P (n div 2) \<Longrightarrow> P n"
     3.6    shows "P n"
     3.7 -using `n > 0` proof (induct n rule: log.induct)
     3.8 +using \<open>n > 0\<close> proof (induct n rule: log.induct)
     3.9    fix n
    3.10    assume "\<not> n < 2 \<Longrightarrow>
    3.11            0 < n div 2 \<Longrightarrow> P (n div 2)"
    3.12 @@ -30,7 +30,7 @@
    3.13    proof (cases "n = 1")
    3.14      case True with one show ?thesis by simp
    3.15    next
    3.16 -    case False with `n > 0` have "n \<ge> 2" by auto
    3.17 +    case False with \<open>n > 0\<close> have "n \<ge> 2" by auto
    3.18      moreover with * have "P (n div 2)" .
    3.19      ultimately show ?thesis by (rule double)
    3.20    qed
    3.21 @@ -82,7 +82,7 @@
    3.22        with mn2 have "n \<ge> 2" by arith
    3.23        from True have m2_0: "m div 2 \<noteq> 0" by arith
    3.24        with mn2 have n2_0: "n div 2 \<noteq> 0" by arith
    3.25 -      from `\<not> m < 2` "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
    3.26 +      from \<open>\<not> m < 2\<close> "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast
    3.27        with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp
    3.28        with m2_0 n2_0 \<open>m \<ge> 2\<close> \<open>n \<ge> 2\<close> show ?thesis by (simp only: log_rec [of m] log_rec [of n]) simp
    3.29      qed
    3.30 @@ -100,9 +100,9 @@
    3.31    with log_mono have "log n \<ge> Suc 0"
    3.32      by (simp add: log.simps)
    3.33    assume "2 ^ log (n div 2) \<le> n div 2"
    3.34 -  with `n \<ge> 2` have "2 ^ (log n - Suc 0) \<le> n div 2" by simp
    3.35 +  with \<open>n \<ge> 2\<close> have "2 ^ (log n - Suc 0) \<le> n div 2" by simp
    3.36    then have "2 ^ (log n - Suc 0) * 2 ^ 1 \<le> n div 2 * 2" by simp
    3.37 -  with `log n \<ge> Suc 0` have "2 ^ log n \<le> n div 2 * 2"
    3.38 +  with \<open>log n \<ge> Suc 0\<close> have "2 ^ log n \<le> n div 2 * 2"
    3.39      unfolding power_add [symmetric] by simp
    3.40    also have "n div 2 * 2 \<le> n" by (cases "even n") simp_all
    3.41    finally show "2 ^ log n \<le> n" .
     4.1 --- a/src/HOL/Library/Function_Growth.thy	Wed Dec 30 11:32:56 2015 +0100
     4.2 +++ b/src/HOL/Library/Function_Growth.thy	Wed Dec 30 11:37:29 2015 +0100
     4.3 @@ -37,7 +37,7 @@
     4.4  proof -
     4.5    def q == "m - n"
     4.6    moreover with assms have "m = q + n" by (simp add: q_def)
     4.7 -  ultimately show ?thesis using `a \<noteq> 0` by (simp add: power_add)
     4.8 +  ultimately show ?thesis using \<open>a \<noteq> 0\<close> by (simp add: power_add)
     4.9  qed
    4.10  
    4.11  
    4.12 @@ -335,14 +335,14 @@
    4.13    proof
    4.14      show "(\<lambda>n. f n + k) \<lesssim> f"
    4.15      proof
    4.16 -      from `\<exists>n. f n > 0` obtain n where "f n > 0" ..
    4.17 +      from \<open>\<exists>n. f n > 0\<close> obtain n where "f n > 0" ..
    4.18        have "\<forall>m>n. f m + k \<le> Suc k * f m"
    4.19        proof (rule allI, rule impI)
    4.20          fix m
    4.21          assume "n < m"
    4.22 -        with `mono f` have "f n \<le> f m"
    4.23 +        with \<open>mono f\<close> have "f n \<le> f m"
    4.24            using less_imp_le_nat monoE by blast
    4.25 -        with  `0 < f n` have "0 < f m" by auto
    4.26 +        with  \<open>0 < f n\<close> have "0 < f m" by auto
    4.27          then obtain l where "f m = Suc l" by (cases "f m") simp_all
    4.28          then show "f m + k \<le> Suc k * f m" by simp
    4.29        qed
    4.30 @@ -366,7 +366,7 @@
    4.31      assume "\<not> (\<exists>n. 0 < f n)"
    4.32      then have "\<And>n. f n = 0" by simp
    4.33      then have "f 0 = f 1" by simp
    4.34 -    moreover from `strict_mono f` have "f 0 < f 1"
    4.35 +    moreover from \<open>strict_mono f\<close> have "f 0 < f 1"
    4.36        by (simp add: strict_mono_def) 
    4.37      ultimately show False by simp
    4.38    qed
     5.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Wed Dec 30 11:32:56 2015 +0100
     5.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Wed Dec 30 11:37:29 2015 +0100
     5.3 @@ -2,7 +2,7 @@
     5.4      Author:     Fabian Immler, TU M√ľnchen
     5.5  *)
     5.6  
     5.7 -section {* Bounded Linear Function *}
     5.8 +section \<open>Bounded Linear Function\<close>
     5.9  
    5.10  theory Bounded_Linear_Function
    5.11  imports
    5.12 @@ -10,7 +10,7 @@
    5.13    Operator_Norm
    5.14  begin
    5.15  
    5.16 -subsection {* Intro rules for @{term bounded_linear} *}
    5.17 +subsection \<open>Intro rules for @{term bounded_linear}\<close>
    5.18  
    5.19  named_theorems bounded_linear_intros
    5.20  
    5.21 @@ -218,7 +218,7 @@
    5.22        proof (rule CauchyI)
    5.23          fix e::real
    5.24          assume "0 < e"
    5.25 -        from CauchyD[OF `Cauchy X` `0 < e`] obtain M
    5.26 +        from CauchyD[OF \<open>Cauchy X\<close> \<open>0 < e\<close>] obtain M
    5.27            where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
    5.28            by auto
    5.29          show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m x - X n x) < e"
    5.30 @@ -230,7 +230,7 @@
    5.31            also have "\<dots> \<le> norm (X m - X n) * norm x"
    5.32               by (rule norm_blinfun)
    5.33            also have "\<dots> \<le> norm (X m - X n) * 1"
    5.34 -            using `norm x \<le> 1` norm_ge_zero by (rule mult_left_mono)
    5.35 +            using \<open>norm x \<le> 1\<close> norm_ge_zero by (rule mult_left_mono)
    5.36            also have "\<dots> = norm (X m - X n)" by simp
    5.37            also have "\<dots> < e" using le by fact
    5.38            finally show "norm (X m x - X n x) < e" .
    5.39 @@ -257,7 +257,7 @@
    5.40    proof (rule CauchyI)
    5.41      fix e::real
    5.42      assume "e > 0"
    5.43 -    from CauchyD[OF `Cauchy X` `0 < e`] obtain M
    5.44 +    from CauchyD[OF \<open>Cauchy X\<close> \<open>0 < e\<close>] obtain M
    5.45        where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < e"
    5.46        by auto
    5.47      show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (norm (X m) - norm (X n)) < e"
    5.48 @@ -297,8 +297,8 @@
    5.49    proof (rule LIMSEQ_I)
    5.50      fix r::real assume "r > 0"
    5.51      def r' \<equiv> "r / 2"
    5.52 -    have "0 < r'" "r' < r" using `r > 0` by (simp_all add: r'_def)
    5.53 -    from CauchyD[OF `Cauchy X` `r' > 0`]
    5.54 +    have "0 < r'" "r' < r" using \<open>r > 0\<close> by (simp_all add: r'_def)
    5.55 +    from CauchyD[OF \<open>Cauchy X\<close> \<open>r' > 0\<close>]
    5.56      obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> norm (X m - X n) < r'"
    5.57        by metis
    5.58      show "\<exists>no. \<forall>n\<ge>no. norm (X n - Blinfun v) < r"
    5.59 @@ -324,16 +324,16 @@
    5.60            by (auto intro!: tendsto_intros Bv)
    5.61          show "norm ((X n - Blinfun v) x) \<le> r' * norm x"
    5.62            by (auto intro!: tendsto_ge_const tendsto_v ev_le simp: blinfun.bilinear_simps)
    5.63 -      qed (simp add: `0 < r'` less_imp_le)
    5.64 +      qed (simp add: \<open>0 < r'\<close> less_imp_le)
    5.65        thus "norm (X n - Blinfun v) < r"
    5.66 -        by (metis `r' < r` le_less_trans)
    5.67 +        by (metis \<open>r' < r\<close> le_less_trans)
    5.68      qed
    5.69    qed
    5.70    thus "convergent X"
    5.71      by (rule convergentI)
    5.72  qed
    5.73  
    5.74 -subsection {* On Euclidean Space *}
    5.75 +subsection \<open>On Euclidean Space\<close>
    5.76  
    5.77  lemma Zfun_setsum:
    5.78    assumes "finite s"
    5.79 @@ -462,7 +462,7 @@
    5.80    "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)"
    5.81    by auto
    5.82  
    5.83 -text {* TODO: generalize this and @{thm compact_lemma}?! *}
    5.84 +text \<open>TODO: generalize this and @{thm compact_lemma}?!\<close>
    5.85  lemma compact_blinfun_lemma:
    5.86    fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
    5.87    assumes "bounded (range f)"
    5.88 @@ -484,7 +484,7 @@
    5.89      have k[intro]: "k \<in> Basis"
    5.90        using insert by auto
    5.91      have s': "bounded ((\<lambda>x. blinfun_apply x k) ` range f)"
    5.92 -      using `bounded (range f)`
    5.93 +      using \<open>bounded (range f)\<close>
    5.94        by (auto intro!: bounded_linear_image bounded_linear_intros)
    5.95      obtain l1::"'a \<Rightarrow>\<^sub>L 'b" and r1 where r1: "subseq r1"
    5.96        and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) i) (l1 i) < e) sequentially"
    5.97 @@ -506,9 +506,9 @@
    5.98      {
    5.99        fix e::real
   5.100        assume "e > 0"
   5.101 -      from lr1 `e > 0` have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n)  i) (l1  i) < e) sequentially"
   5.102 +      from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n)  i) (l1  i) < e) sequentially"
   5.103          by blast
   5.104 -      from lr2 `e > 0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n))  k) l2 < e) sequentially"
   5.105 +      from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n))  k) l2 < e) sequentially"
   5.106          by (rule tendstoD)
   5.107        from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n))  i) (l1  i) < e) sequentially"
   5.108          by (rule eventually_subseq)
   5.109 @@ -538,7 +538,7 @@
   5.110    apply (simp add: blinfun.bilinear_simps)
   5.111    done
   5.112  
   5.113 -text {* TODO: generalize (via @{thm compact_cball})? *}
   5.114 +text \<open>TODO: generalize (via @{thm compact_cball})?\<close>
   5.115  instance blinfun :: (euclidean_space, euclidean_space) heine_borel
   5.116  proof
   5.117    fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
     6.1 --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Dec 30 11:32:56 2015 +0100
     6.2 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy	Wed Dec 30 11:37:29 2015 +0100
     6.3 @@ -6049,7 +6049,7 @@
     6.4       apply (clarsimp simp del: divide_const_simps)
     6.5       apply (metis add.commute dist_commute le_less_trans mem_ball real_gt_half_sum w)
     6.6       done
     6.7 -  --\<open>Replacing @{term r} and the original (weak) premises\<close>
     6.8 +  \<comment>\<open>Replacing @{term r} and the original (weak) premises\<close>
     6.9    obtain r where "0 < r" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
    6.10      apply (rule that [of "(r + dist w z) / 2"])
    6.11        apply (simp_all add: fh')
     7.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Dec 30 11:32:56 2015 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed Dec 30 11:37:29 2015 +0100
     7.3 @@ -261,7 +261,7 @@
     7.4  
     7.5  subsection\<open>Holomorphic functions\<close>
     7.6  
     7.7 -text{*Could be generalized to real normed fields, but in practice that would only include the reals*}
     7.8 +text\<open>Could be generalized to real normed fields, but in practice that would only include the reals\<close>
     7.9  definition complex_differentiable :: "[complex \<Rightarrow> complex, complex filter] \<Rightarrow> bool"
    7.10             (infixr "(complex'_differentiable)" 50)
    7.11    where "f complex_differentiable F \<equiv> \<exists>f'. (f has_field_derivative f') F"
     8.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Dec 30 11:32:56 2015 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Wed Dec 30 11:37:29 2015 +0100
     8.3 @@ -2471,7 +2471,7 @@
     8.4      unfolding has_vector_derivative_def has_derivative_iff_norm
     8.5      using assms by (intro conj_cong Lim_cong_within refl) auto
     8.6    then show ?thesis
     8.7 -    using has_vector_derivative_within_subset[OF f `s \<subseteq> t`] by simp
     8.8 +    using has_vector_derivative_within_subset[OF f \<open>s \<subseteq> t\<close>] by simp
     8.9  qed
    8.10  
    8.11  lemma has_vector_derivative_transform_within:
     9.1 --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Wed Dec 30 11:32:56 2015 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Wed Dec 30 11:37:29 2015 +0100
     9.3 @@ -189,13 +189,13 @@
     9.4        by (metis bounded_linear_mult_const f)
     9.5      from onorm_scaleR_left_lemma[OF this, of "inverse (norm f)"]
     9.6      have "onorm r \<le> onorm (\<lambda>x. r x * norm f) * inverse (norm f)"
     9.7 -      using `f \<noteq> 0`
     9.8 +      using \<open>f \<noteq> 0\<close>
     9.9        by (simp add: inverse_eq_divide)
    9.10      also have "onorm (\<lambda>x. r x * norm f) \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
    9.11        by (rule onorm_bound)
    9.12          (auto simp: abs_mult bl1 onorm_pos_le intro!: order_trans[OF _ onorm])
    9.13      finally show "onorm r * norm f \<le> onorm (\<lambda>x. r x *\<^sub>R f)"
    9.14 -      using `f \<noteq> 0`
    9.15 +      using \<open>f \<noteq> 0\<close>
    9.16        by (simp add: inverse_eq_divide pos_le_divide_eq mult.commute)
    9.17    qed
    9.18  qed (simp add: onorm_zero)
    10.1 --- a/src/HOL/NSA/CLim.thy	Wed Dec 30 11:32:56 2015 +0100
    10.2 +++ b/src/HOL/NSA/CLim.thy	Wed Dec 30 11:37:29 2015 +0100
    10.3 @@ -4,7 +4,7 @@
    10.4      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    10.5  *)
    10.6  
    10.7 -section{*Limits, Continuity and Differentiation for Complex Functions*}
    10.8 +section\<open>Limits, Continuity and Differentiation for Complex Functions\<close>
    10.9  
   10.10  theory CLim
   10.11  imports CStar
   10.12 @@ -18,7 +18,7 @@
   10.13       "x \<noteq> (0::complex) \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
   10.14  by (simp add: numeral_2_eq_2)
   10.15  
   10.16 -text{*Changing the quantified variable. Install earlier?*}
   10.17 +text\<open>Changing the quantified variable. Install earlier?\<close>
   10.18  lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))"
   10.19  apply auto 
   10.20  apply (drule_tac x="x+a" in spec) 
   10.21 @@ -34,7 +34,7 @@
   10.22  done
   10.23  
   10.24  
   10.25 -subsection{*Limit of Complex to Complex Function*}
   10.26 +subsection\<open>Limit of Complex to Complex Function\<close>
   10.27  
   10.28  lemma NSLIM_Re: "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L ==> (%x. Re(f x)) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S Re(L)"
   10.29  by (simp add: NSLIM_def starfunC_approx_Re_Im_iff 
   10.30 @@ -108,13 +108,13 @@
   10.31  by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
   10.32  
   10.33  
   10.34 -subsection{*Continuity*}
   10.35 +subsection\<open>Continuity\<close>
   10.36  
   10.37  lemma NSLIM_isContc_iff:
   10.38       "(f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S f a) = ((%h. f(a + h)) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S f a)"
   10.39  by (rule NSLIM_h_iff)
   10.40  
   10.41 -subsection{*Functions from Complex to Reals*}
   10.42 +subsection\<open>Functions from Complex to Reals\<close>
   10.43  
   10.44  lemma isNSContCR_cmod [simp]: "isNSCont cmod (a)"
   10.45  by (auto intro: approx_hnorm
   10.46 @@ -134,7 +134,7 @@
   10.47    shows "isCont f a ==> isCont (%x. Im (f x)) a"
   10.48  by (simp add: isCont_def LIM_Im)
   10.49  
   10.50 -subsection{* Differentiation of Natural Number Powers*}
   10.51 +subsection\<open>Differentiation of Natural Number Powers\<close>
   10.52  
   10.53  lemma CDERIV_pow [simp]:
   10.54       "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
   10.55 @@ -145,11 +145,11 @@
   10.56  apply (auto simp add: ac_simps)
   10.57  done
   10.58  
   10.59 -text{*Nonstandard version*}
   10.60 +text\<open>Nonstandard version\<close>
   10.61  lemma NSCDERIV_pow: "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
   10.62      by (metis CDERIV_pow NSDERIV_DERIV_iff One_nat_def)
   10.63  
   10.64 -text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
   10.65 +text\<open>Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero\<close>
   10.66  lemma NSCDERIV_inverse:
   10.67       "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- ((inverse x)\<^sup>2))"
   10.68  unfolding numeral_2_eq_2
   10.69 @@ -161,7 +161,7 @@
   10.70  by (rule DERIV_inverse)
   10.71  
   10.72  
   10.73 -subsection{*Derivative of Reciprocals (Function @{term inverse})*}
   10.74 +subsection\<open>Derivative of Reciprocals (Function @{term inverse})\<close>
   10.75  
   10.76  lemma CDERIV_inverse_fun:
   10.77       "[| DERIV f x :> d; f(x) \<noteq> (0::complex) |]
   10.78 @@ -176,7 +176,7 @@
   10.79  by (rule NSDERIV_inverse_fun)
   10.80  
   10.81  
   10.82 -subsection{* Derivative of Quotient*}
   10.83 +subsection\<open>Derivative of Quotient\<close>
   10.84  
   10.85  lemma CDERIV_quotient:
   10.86       "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> (0::complex) |]
   10.87 @@ -191,7 +191,7 @@
   10.88  by (rule NSDERIV_quotient)
   10.89  
   10.90  
   10.91 -subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*}
   10.92 +subsection\<open>Caratheodory Formulation of Derivative at a Point: Standard Proof\<close>
   10.93  
   10.94  lemma CARAT_CDERIVD:
   10.95       "(\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l
    11.1 --- a/src/HOL/NSA/CStar.thy	Wed Dec 30 11:32:56 2015 +0100
    11.2 +++ b/src/HOL/NSA/CStar.thy	Wed Dec 30 11:37:29 2015 +0100
    11.3 @@ -3,14 +3,14 @@
    11.4      Copyright   : 2001 University of Edinburgh
    11.5  *)
    11.6  
    11.7 -section{*Star-transforms in NSA, Extending Sets of Complex Numbers
    11.8 -      and Complex Functions*}
    11.9 +section\<open>Star-transforms in NSA, Extending Sets of Complex Numbers
   11.10 +      and Complex Functions\<close>
   11.11  
   11.12  theory CStar
   11.13  imports NSCA
   11.14  begin
   11.15  
   11.16 -subsection{*Properties of the *-Transform Applied to Sets of Reals*}
   11.17 +subsection\<open>Properties of the *-Transform Applied to Sets of Reals\<close>
   11.18  
   11.19  lemma STARC_hcomplex_of_complex_Int:
   11.20       "*s* X Int SComplex = hcomplex_of_complex ` X"
   11.21 @@ -20,7 +20,7 @@
   11.22       "x \<notin> hcomplex_of_complex ` A ==> \<forall>y \<in> A. x \<noteq> hcomplex_of_complex y"
   11.23  by auto
   11.24  
   11.25 -subsection{*Theorems about Nonstandard Extensions of Functions*}
   11.26 +subsection\<open>Theorems about Nonstandard Extensions of Functions\<close>
   11.27  
   11.28  lemma starfunC_hcpow: "!!Z. ( *f* (%z. z ^ n)) Z = Z pow hypnat_of_nat n"
   11.29  by transfer (rule refl)
   11.30 @@ -28,7 +28,7 @@
   11.31  lemma starfunCR_cmod: "*f* cmod = hcmod"
   11.32  by transfer (rule refl)
   11.33  
   11.34 -subsection{*Internal Functions - Some Redundancy With *f* Now*}
   11.35 +subsection\<open>Internal Functions - Some Redundancy With *f* Now\<close>
   11.36  
   11.37  (** subtraction: ( *fn) - ( *gn) = *(fn - gn) **)
   11.38  (*
    12.1 --- a/src/HOL/NSA/Examples/NSPrimes.thy	Wed Dec 30 11:32:56 2015 +0100
    12.2 +++ b/src/HOL/NSA/Examples/NSPrimes.thy	Wed Dec 30 11:37:29 2015 +0100
    12.3 @@ -4,14 +4,14 @@
    12.4      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    12.5  *)
    12.6  
    12.7 -section{*The Nonstandard Primes as an Extension of the Prime Numbers*}
    12.8 +section\<open>The Nonstandard Primes as an Extension of the Prime Numbers\<close>
    12.9  
   12.10  theory NSPrimes
   12.11  imports "~~/src/HOL/Number_Theory/UniqueFactorization" "../Hyperreal"
   12.12  begin
   12.13  
   12.14 -text{*These can be used to derive an alternative proof of the infinitude of
   12.15 -primes by considering a property of nonstandard sets.*}
   12.16 +text\<open>These can be used to derive an alternative proof of the infinitude of
   12.17 +primes by considering a property of nonstandard sets.\<close>
   12.18  
   12.19  definition
   12.20    starprime :: "hypnat set" where
   12.21 @@ -55,8 +55,8 @@
   12.22  done
   12.23  
   12.24  
   12.25 -text{*The nonstandard extension of the set prime numbers consists of precisely
   12.26 -those hypernaturals exceeding 1 that have no nontrivial factors*}
   12.27 +text\<open>The nonstandard extension of the set prime numbers consists of precisely
   12.28 +those hypernaturals exceeding 1 that have no nontrivial factors\<close>
   12.29  
   12.30  (* Goldblatt: Exercise 5.11(3a) - p 57  *)
   12.31  lemma starprime:
   12.32 @@ -73,7 +73,7 @@
   12.33  by (rule starset_finite)
   12.34  
   12.35  
   12.36 -subsection{*Another characterization of infinite set of natural numbers*}
   12.37 +subsection\<open>Another characterization of infinite set of natural numbers\<close>
   12.38  
   12.39  lemma finite_nat_set_bounded: "finite N ==> \<exists>n. (\<forall>i \<in> N. i<(n::nat))"
   12.40  apply (erule_tac F = N in finite_induct, auto)
   12.41 @@ -103,7 +103,7 @@
   12.42  by (auto simp add: finite_nat_set_bounded_iff2 not_le)
   12.43  
   12.44  
   12.45 -subsection{*An injective function cannot define an embedded natural number*}
   12.46 +subsection\<open>An injective function cannot define an embedded natural number\<close>
   12.47  
   12.48  lemma lemma_infinite_set_singleton: "\<forall>m n. m \<noteq> n --> f n \<noteq> f m
   12.49        ==>  {n. f n = N} = {} |  (\<exists>m. {n. f n = N} = {m})"
   12.50 @@ -197,7 +197,7 @@
   12.51  apply (rule_tac [4] injf_max_order_preserving, auto)
   12.52  done
   12.53  
   12.54 -text{*Only need the existence of an injective function from N to A for proof*}
   12.55 +text\<open>Only need the existence of an injective function from N to A for proof\<close>
   12.56  
   12.57  lemma hypnat_infinite_has_nonstandard:
   12.58       "~ finite A ==> hypnat_of_nat ` A < ( *s* A)"
   12.59 @@ -223,7 +223,7 @@
   12.60  apply (auto simp add: finite_starsetNat_iff [symmetric])
   12.61  done
   12.62  
   12.63 -subsection{*Existence of Infinitely Many Primes: a Nonstandard Proof*}
   12.64 +subsection\<open>Existence of Infinitely Many Primes: a Nonstandard Proof\<close>
   12.65  
   12.66  lemma lemma_not_dvd_hypnat_one [simp]: "~ (\<forall>n \<in> - {0}. hypnat_of_nat n dvd 1)"
   12.67  apply auto
   12.68 @@ -259,7 +259,7 @@
   12.69  lemma hdvd_one_eq_one: "!!x. x dvd (1::hypnat) ==> x = 1"
   12.70  by (transfer, rule gcd_lcm_complete_lattice_nat.le_bot)
   12.71  
   12.72 -text{*Already proved as @{text primes_infinite}, but now using non-standard naturals.*}
   12.73 +text\<open>Already proved as \<open>primes_infinite\<close>, but now using non-standard naturals.\<close>
   12.74  theorem not_finite_prime: "~ finite {p::nat. prime p}"
   12.75  apply (rule hypnat_infinite_has_nonstandard_iff [THEN iffD2])
   12.76  using hypnat_dvd_all_hypnat_of_nat
    13.1 --- a/src/HOL/NSA/Free_Ultrafilter.thy	Wed Dec 30 11:32:56 2015 +0100
    13.2 +++ b/src/HOL/NSA/Free_Ultrafilter.thy	Wed Dec 30 11:37:29 2015 +0100
    13.3 @@ -4,15 +4,15 @@
    13.4      Author:     Brian Huffman
    13.5  *) 
    13.6  
    13.7 -section {* Filters and Ultrafilters *}
    13.8 +section \<open>Filters and Ultrafilters\<close>
    13.9  
   13.10  theory Free_Ultrafilter
   13.11  imports "~~/src/HOL/Library/Infinite_Set"
   13.12  begin
   13.13  
   13.14 -subsection {* Definitions and basic properties *}
   13.15 +subsection \<open>Definitions and basic properties\<close>
   13.16  
   13.17 -subsubsection {* Ultrafilters *}
   13.18 +subsubsection \<open>Ultrafilters\<close>
   13.19  
   13.20  locale ultrafilter =
   13.21    fixes F :: "'a filter"
   13.22 @@ -43,17 +43,17 @@
   13.23  
   13.24  end
   13.25  
   13.26 -subsection {* Maximal filter = Ultrafilter *}
   13.27 +subsection \<open>Maximal filter = Ultrafilter\<close>
   13.28  
   13.29 -text {*
   13.30 +text \<open>
   13.31     A filter F is an ultrafilter iff it is a maximal filter,
   13.32     i.e. whenever G is a filter and @{term "F \<subseteq> G"} then @{term "F = G"}
   13.33 -*}
   13.34 -text {*
   13.35 +\<close>
   13.36 +text \<open>
   13.37    Lemmas that shows existence of an extension to what was assumed to
   13.38    be a maximal filter. Will be used to derive contradiction in proof of
   13.39    property of ultrafilter.
   13.40 -*}
   13.41 +\<close>
   13.42  
   13.43  lemma extend_filter:
   13.44    "frequently P F \<Longrightarrow> inf F (principal {x. P x}) \<noteq> bot"
   13.45 @@ -92,7 +92,7 @@
   13.46               intro!: eventually_frequently G proper)
   13.47  qed fact
   13.48  
   13.49 -subsection {* Ultrafilter Theorem *}
   13.50 +subsection \<open>Ultrafilter Theorem\<close>
   13.51  
   13.52  text "A local context makes proof of ultrafilter Theorem more modular"
   13.53  
   13.54 @@ -124,7 +124,7 @@
   13.55            unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def)
   13.56          with c have 1: "Inf c \<noteq> bot"
   13.57            by (simp add: bot_notin_R)
   13.58 -        from `c \<noteq> {}` obtain x where "x \<in> c" by auto
   13.59 +        from \<open>c \<noteq> {}\<close> obtain x where "x \<in> c" by auto
   13.60          with c have 2: "Inf c \<le> F"
   13.61            by (auto intro!: Inf_lower2[of x] simp: Chains_def)
   13.62          note 1 2 }
   13.63 @@ -148,9 +148,9 @@
   13.64      by (intro exI[of _ U] conjI max_filter_ultrafilter) auto
   13.65  qed
   13.66  
   13.67 -subsubsection {* Free Ultrafilters *}
   13.68 +subsubsection \<open>Free Ultrafilters\<close>
   13.69  
   13.70 -text {* There exists a free ultrafilter on any infinite set *}
   13.71 +text \<open>There exists a free ultrafilter on any infinite set\<close>
   13.72  
   13.73  locale freeultrafilter = ultrafilter +
   13.74    assumes infinite: "eventually P F \<Longrightarrow> infinite {x. P x}"
   13.75 @@ -190,7 +190,7 @@
   13.76      with proper have "frequently P U"
   13.77        by (rule eventually_frequently)
   13.78      then have "frequently P cofinite"
   13.79 -      using `U \<le> cofinite` by (simp add: le_filter_frequently)
   13.80 +      using \<open>U \<le> cofinite\<close> by (simp add: le_filter_frequently)
   13.81      then show "infinite {x. P x}"
   13.82        by (simp add: frequently_cofinite)
   13.83    qed
    14.1 --- a/src/HOL/NSA/HDeriv.thy	Wed Dec 30 11:32:56 2015 +0100
    14.2 +++ b/src/HOL/NSA/HDeriv.thy	Wed Dec 30 11:37:29 2015 +0100
    14.3 @@ -4,13 +4,13 @@
    14.4      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    14.5  *)
    14.6  
    14.7 -section{* Differentiation (Nonstandard) *}
    14.8 +section\<open>Differentiation (Nonstandard)\<close>
    14.9  
   14.10  theory HDeriv
   14.11  imports HLim
   14.12  begin
   14.13  
   14.14 -text{*Nonstandard Definitions*}
   14.15 +text\<open>Nonstandard Definitions\<close>
   14.16  
   14.17  definition
   14.18    nsderiv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool"
   14.19 @@ -30,7 +30,7 @@
   14.20             inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
   14.21  
   14.22  
   14.23 -subsection {* Derivatives *}
   14.24 +subsection \<open>Derivatives\<close>
   14.25  
   14.26  lemma DERIV_NS_iff:
   14.27        "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D)"
   14.28 @@ -66,9 +66,9 @@
   14.29  apply (simp add: of_hypreal_eq_0_iff hypreal_epsilon_not_zero)
   14.30  done
   14.31  
   14.32 -text {*First NSDERIV in terms of NSLIM*}
   14.33 +text \<open>First NSDERIV in terms of NSLIM\<close>
   14.34  
   14.35 -text{*first equivalence *}
   14.36 +text\<open>first equivalence\<close>
   14.37  lemma NSDERIV_NSLIM_iff:
   14.38        "(NSDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D)"
   14.39  apply (simp add: nsderiv_def NSLIM_def, auto)
   14.40 @@ -78,7 +78,7 @@
   14.41  apply (auto simp add: mem_infmal_iff starfun_lambda_cancel)
   14.42  done
   14.43  
   14.44 -text{*second equivalence *}
   14.45 +text\<open>second equivalence\<close>
   14.46  lemma NSDERIV_NSLIM_iff2:
   14.47       "(NSDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) \<midarrow>x\<rightarrow>\<^sub>N\<^sub>S D)"
   14.48    by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff LIM_NSLIM_iff [symmetric])
   14.49 @@ -136,8 +136,8 @@
   14.50  apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] simp add: mult.assoc)
   14.51  done
   14.52  
   14.53 -text{*Differentiability implies continuity
   14.54 -         nice and simple "algebraic" proof*}
   14.55 +text\<open>Differentiability implies continuity
   14.56 +         nice and simple "algebraic" proof\<close>
   14.57  lemma NSDERIV_isNSCont: "NSDERIV f x :> D ==> isNSCont f x"
   14.58  apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def)
   14.59  apply (drule approx_minus_iff [THEN iffD1])
   14.60 @@ -155,16 +155,16 @@
   14.61              intro: approx_trans approx_minus_iff [THEN iffD2])
   14.62  done
   14.63  
   14.64 -text{*Differentiation rules for combinations of functions
   14.65 +text\<open>Differentiation rules for combinations of functions
   14.66        follow from clear, straightforard, algebraic
   14.67 -      manipulations*}
   14.68 -text{*Constant function*}
   14.69 +      manipulations\<close>
   14.70 +text\<open>Constant function\<close>
   14.71  
   14.72  (* use simple constant nslimit theorem *)
   14.73  lemma NSDERIV_const [simp]: "(NSDERIV (%x. k) x :> 0)"
   14.74  by (simp add: NSDERIV_NSLIM_iff)
   14.75  
   14.76 -text{*Sum of functions- proved easily*}
   14.77 +text\<open>Sum of functions- proved easily\<close>
   14.78  
   14.79  lemma NSDERIV_add: "[| NSDERIV f x :> Da;  NSDERIV g x :> Db |]
   14.80        ==> NSDERIV (%x. f x + g x) x :> Da + Db"
   14.81 @@ -174,8 +174,8 @@
   14.82  apply (auto simp add: ac_simps algebra_simps)
   14.83  done
   14.84  
   14.85 -text{*Product of functions - Proof is trivial but tedious
   14.86 -  and long due to rearrangement of terms*}
   14.87 +text\<open>Product of functions - Proof is trivial but tedious
   14.88 +  and long due to rearrangement of terms\<close>
   14.89  
   14.90  lemma lemma_nsderiv1:
   14.91    fixes a b c d :: "'a::comm_ring star"
   14.92 @@ -216,7 +216,7 @@
   14.93            simp add: add.assoc [symmetric])
   14.94  done
   14.95  
   14.96 -text{*Multiplying by a constant*}
   14.97 +text\<open>Multiplying by a constant\<close>
   14.98  lemma NSDERIV_cmult: "NSDERIV f x :> D
   14.99        ==> NSDERIV (%x. c * f x) x :> c*D"
  14.100  apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff
  14.101 @@ -224,7 +224,7 @@
  14.102  apply (erule NSLIM_const [THEN NSLIM_mult])
  14.103  done
  14.104  
  14.105 -text{*Negation of function*}
  14.106 +text\<open>Negation of function\<close>
  14.107  lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. -(f x)) x :> -D"
  14.108  proof (simp add: NSDERIV_NSLIM_iff)
  14.109    assume "(\<lambda>h. (f (x + h) - f x) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S D"
  14.110 @@ -238,7 +238,7 @@
  14.111      (\<lambda>h. (f x - f (x + h)) / h) \<midarrow>0\<rightarrow>\<^sub>N\<^sub>S - D" by simp
  14.112  qed
  14.113  
  14.114 -text{*Subtraction*}
  14.115 +text\<open>Subtraction\<close>
  14.116  lemma NSDERIV_add_minus: "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] ==> NSDERIV (%x. f x + -g x) x :> Da + -Db"
  14.117  by (blast dest: NSDERIV_add NSDERIV_minus)
  14.118  
  14.119 @@ -246,12 +246,12 @@
  14.120    "NSDERIV f x :> Da \<Longrightarrow> NSDERIV g x :> Db \<Longrightarrow> NSDERIV (\<lambda>x. f x - g x) x :> Da-Db"
  14.121    using NSDERIV_add_minus [of f x Da g Db] by simp
  14.122  
  14.123 -text{*  Similarly to the above, the chain rule admits an entirely
  14.124 +text\<open>Similarly to the above, the chain rule admits an entirely
  14.125     straightforward derivation. Compare this with Harrison's
  14.126     HOL proof of the chain rule, which proved to be trickier and
  14.127     required an alternative characterisation of differentiability-
  14.128     the so-called Carathedory derivative. Our main problem is
  14.129 -   manipulation of terms.*}
  14.130 +   manipulation of terms.\<close>
  14.131  
  14.132  (* lemmas *)
  14.133  
  14.134 @@ -312,7 +312,7 @@
  14.135    thus ?thesis by (simp add: mult.assoc)
  14.136  qed
  14.137  
  14.138 -text{*This proof uses both definitions of differentiability.*}
  14.139 +text\<open>This proof uses both definitions of differentiability.\<close>
  14.140  lemma NSDERIV_chain: "[| NSDERIV f (g x) :> Da; NSDERIV g x :> Db |]
  14.141        ==> NSDERIV (f o g) x :> Da * Db"
  14.142  apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def
  14.143 @@ -331,7 +331,7 @@
  14.144  apply (blast intro: NSDERIVD2)
  14.145  done
  14.146  
  14.147 -text{*Differentiation of natural number powers*}
  14.148 +text\<open>Differentiation of natural number powers\<close>
  14.149  lemma NSDERIV_Id [simp]: "NSDERIV (%x. x) x :> 1"
  14.150  by (simp add: NSDERIV_NSLIM_iff NSLIM_def del: divide_self_if)
  14.151  
  14.152 @@ -340,7 +340,7 @@
  14.153  
  14.154  lemma NSDERIV_inverse:
  14.155    fixes x :: "'a::real_normed_field"
  14.156 -  assumes "x \<noteq> 0" -- {* can't get rid of @{term "x \<noteq> 0"} because it isn't continuous at zero *}
  14.157 +  assumes "x \<noteq> 0" \<comment> \<open>can't get rid of @{term "x \<noteq> 0"} because it isn't continuous at zero\<close>
  14.158    shows "NSDERIV (\<lambda>x. inverse x) x :> - (inverse x ^ Suc (Suc 0))"
  14.159  proof -
  14.160    { fix h :: "'a star"
  14.161 @@ -355,7 +355,7 @@
  14.162          dest!: hypreal_of_real_HFinite_diff_Infinitesimal
  14.163          simp add: inverse_minus_eq [symmetric] HFinite_minus_iff)
  14.164        done
  14.165 -    moreover from not_0 `h \<noteq> 0` assms
  14.166 +    moreover from not_0 \<open>h \<noteq> 0\<close> assms
  14.167        have "inverse (- (h * star_of x) + - (star_of x * star_of x)) =
  14.168          (inverse (star_of x + h) - inverse (star_of x)) / h"
  14.169        apply (simp add: division_ring_inverse_diff nonzero_inverse_mult_distrib [symmetric]
  14.170 @@ -370,12 +370,12 @@
  14.171    } then show ?thesis by (simp add: nsderiv_def)
  14.172  qed
  14.173  
  14.174 -subsubsection {* Equivalence of NS and Standard definitions *}
  14.175 +subsubsection \<open>Equivalence of NS and Standard definitions\<close>
  14.176  
  14.177  lemma divideR_eq_divide: "x /\<^sub>R y = x / y"
  14.178  by (simp add: divide_inverse mult.commute)
  14.179  
  14.180 -text{*Now equivalence between NSDERIV and DERIV*}
  14.181 +text\<open>Now equivalence between NSDERIV and DERIV\<close>
  14.182  lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)"
  14.183  by (simp add: DERIV_def NSDERIV_NSLIM_iff LIM_NSLIM_iff)
  14.184  
  14.185 @@ -383,7 +383,7 @@
  14.186  lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))"
  14.187  by (simp add: NSDERIV_DERIV_iff DERIV_pow)
  14.188  
  14.189 -text{*Derivative of inverse*}
  14.190 +text\<open>Derivative of inverse\<close>
  14.191  
  14.192  lemma NSDERIV_inverse_fun:
  14.193    fixes x :: "'a::{real_normed_field}"
  14.194 @@ -391,7 +391,7 @@
  14.195        ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))"
  14.196  by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: power_Suc)
  14.197  
  14.198 -text{*Derivative of quotient*}
  14.199 +text\<open>Derivative of quotient\<close>
  14.200  
  14.201  lemma NSDERIV_quotient:
  14.202    fixes x :: "'a::{real_normed_field}"
  14.203 @@ -422,7 +422,7 @@
  14.204      by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong)
  14.205  qed
  14.206  
  14.207 -subsubsection {* Differentiability predicate *}
  14.208 +subsubsection \<open>Differentiability predicate\<close>
  14.209  
  14.210  lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D"
  14.211  by (simp add: NSdifferentiable_def)
  14.212 @@ -431,7 +431,7 @@
  14.213  by (force simp add: NSdifferentiable_def)
  14.214  
  14.215  
  14.216 -subsection {*(NS) Increment*}
  14.217 +subsection \<open>(NS) Increment\<close>
  14.218  lemma incrementI:
  14.219        "f NSdifferentiable x ==>
  14.220        increment f x h = ( *f* f) (hypreal_of_real(x) + h) -
    15.1 --- a/src/HOL/NSA/HLim.thy	Wed Dec 30 11:32:56 2015 +0100
    15.2 +++ b/src/HOL/NSA/HLim.thy	Wed Dec 30 11:37:29 2015 +0100
    15.3 @@ -3,13 +3,13 @@
    15.4      Author:     Lawrence C Paulson
    15.5  *)
    15.6  
    15.7 -section{* Limits and Continuity (Nonstandard) *}
    15.8 +section\<open>Limits and Continuity (Nonstandard)\<close>
    15.9  
   15.10  theory HLim
   15.11  imports Star
   15.12  begin
   15.13  
   15.14 -text{*Nonstandard Definitions*}
   15.15 +text\<open>Nonstandard Definitions\<close>
   15.16  
   15.17  definition
   15.18    NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
   15.19 @@ -19,7 +19,7 @@
   15.20  
   15.21  definition
   15.22    isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
   15.23 -    --{*NS definition dispenses with limit notions*}
   15.24 +    \<comment>\<open>NS definition dispenses with limit notions\<close>
   15.25    "isNSCont f a = (\<forall>y. y @= star_of a -->
   15.26           ( *f* f) y @= star_of (f a))"
   15.27  
   15.28 @@ -28,7 +28,7 @@
   15.29    "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
   15.30  
   15.31  
   15.32 -subsection {* Limits of Functions *}
   15.33 +subsection \<open>Limits of Functions\<close>
   15.34  
   15.35  lemma NSLIM_I:
   15.36    "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
   15.37 @@ -40,8 +40,8 @@
   15.38     \<Longrightarrow> starfun f x \<approx> star_of L"
   15.39  by (simp add: NSLIM_def)
   15.40  
   15.41 -text{*Proving properties of limits using nonstandard definition.
   15.42 -      The properties hold for standard limits as well!*}
   15.43 +text\<open>Proving properties of limits using nonstandard definition.
   15.44 +      The properties hold for standard limits as well!\<close>
   15.45  
   15.46  lemma NSLIM_mult:
   15.47    fixes l m :: "'a::real_normed_algebra"
   15.48 @@ -133,7 +133,7 @@
   15.49  lemma NSLIM_self: "(%x. x) \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S a"
   15.50  by (simp add: NSLIM_def)
   15.51  
   15.52 -subsubsection {* Equivalence of @{term filterlim} and @{term NSLIM} *}
   15.53 +subsubsection \<open>Equivalence of @{term filterlim} and @{term NSLIM}\<close>
   15.54  
   15.55  lemma LIM_NSLIM:
   15.56    assumes f: "f -- a --> L" shows "f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S L"
   15.57 @@ -194,7 +194,7 @@
   15.58  by (blast intro: LIM_NSLIM NSLIM_LIM)
   15.59  
   15.60  
   15.61 -subsection {* Continuity *}
   15.62 +subsection \<open>Continuity\<close>
   15.63  
   15.64  lemma isNSContD:
   15.65    "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
   15.66 @@ -208,32 +208,32 @@
   15.67  apply (case_tac "y = star_of a", auto)
   15.68  done
   15.69  
   15.70 -text{*NS continuity can be defined using NS Limit in
   15.71 -    similar fashion to standard def of continuity*}
   15.72 +text\<open>NS continuity can be defined using NS Limit in
   15.73 +    similar fashion to standard def of continuity\<close>
   15.74  lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f \<midarrow>a\<rightarrow>\<^sub>N\<^sub>S (f a))"
   15.75  by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
   15.76  
   15.77 -text{*Hence, NS continuity can be given
   15.78 -  in terms of standard limit*}
   15.79 +text\<open>Hence, NS continuity can be given
   15.80 +  in terms of standard limit\<close>
   15.81  lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
   15.82  by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
   15.83  
   15.84 -text{*Moreover, it's trivial now that NS continuity
   15.85 -  is equivalent to standard continuity*}
   15.86 +text\<open>Moreover, it's trivial now that NS continuity
   15.87 +  is equivalent to standard continuity\<close>
   15.88  lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
   15.89  apply (simp add: isCont_def)
   15.90  apply (rule isNSCont_LIM_iff)
   15.91  done
   15.92  
   15.93 -text{*Standard continuity ==> NS continuity*}
   15.94 +text\<open>Standard continuity ==> NS continuity\<close>
   15.95  lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
   15.96  by (erule isNSCont_isCont_iff [THEN iffD2])
   15.97  
   15.98 -text{*NS continuity ==> Standard continuity*}
   15.99 +text\<open>NS continuity ==> Standard continuity\<close>
  15.100  lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
  15.101  by (erule isNSCont_isCont_iff [THEN iffD1])
  15.102  
  15.103 -text{*Alternative definition of continuity*}
  15.104 +text\<open>Alternative definition of continuity\<close>
  15.105  
  15.106  (* Prove equivalence between NS limits - *)
  15.107  (* seems easier than using standard def  *)
  15.108 @@ -269,7 +269,7 @@
  15.109  done
  15.110  
  15.111  
  15.112 -subsection {* Uniform Continuity *}
  15.113 +subsection \<open>Uniform Continuity\<close>
  15.114  
  15.115  lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
  15.116  by (simp add: isNSUCont_def)
    16.1 --- a/src/HOL/NSA/HLog.thy	Wed Dec 30 11:32:56 2015 +0100
    16.2 +++ b/src/HOL/NSA/HLog.thy	Wed Dec 30 11:37:29 2015 +0100
    16.3 @@ -3,7 +3,7 @@
    16.4      Copyright   : 2000,2001 University of Edinburgh
    16.5  *)
    16.6  
    16.7 -section{*Logarithms: Non-Standard Version*}
    16.8 +section\<open>Logarithms: Non-Standard Version\<close>
    16.9  
   16.10  theory HLog
   16.11  imports HTranscendental
    17.1 --- a/src/HOL/NSA/HSEQ.thy	Wed Dec 30 11:32:56 2015 +0100
    17.2 +++ b/src/HOL/NSA/HSEQ.thy	Wed Dec 30 11:37:29 2015 +0100
    17.3 @@ -6,7 +6,7 @@
    17.4      Additional contributions by Jeremy Avigad and Brian Huffman
    17.5  *)
    17.6  
    17.7 -section {* Sequences and Convergence (Nonstandard) *}
    17.8 +section \<open>Sequences and Convergence (Nonstandard)\<close>
    17.9  
   17.10  theory HSEQ
   17.11  imports Limits NatStar
   17.12 @@ -15,30 +15,30 @@
   17.13  definition
   17.14    NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
   17.15      ("((_)/ \<longlonglongrightarrow>\<^sub>N\<^sub>S (_))" [60, 60] 60) where
   17.16 -    --{*Nonstandard definition of convergence of sequence*}
   17.17 +    \<comment>\<open>Nonstandard definition of convergence of sequence\<close>
   17.18    "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
   17.19  
   17.20  definition
   17.21    nslim :: "(nat => 'a::real_normed_vector) => 'a" where
   17.22 -    --{*Nonstandard definition of limit using choice operator*}
   17.23 +    \<comment>\<open>Nonstandard definition of limit using choice operator\<close>
   17.24    "nslim X = (THE L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
   17.25  
   17.26  definition
   17.27    NSconvergent :: "(nat => 'a::real_normed_vector) => bool" where
   17.28 -    --{*Nonstandard definition of convergence*}
   17.29 +    \<comment>\<open>Nonstandard definition of convergence\<close>
   17.30    "NSconvergent X = (\<exists>L. X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
   17.31  
   17.32  definition
   17.33    NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
   17.34 -    --{*Nonstandard definition for bounded sequence*}
   17.35 +    \<comment>\<open>Nonstandard definition for bounded sequence\<close>
   17.36    "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
   17.37  
   17.38  definition
   17.39    NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
   17.40 -    --{*Nonstandard definition*}
   17.41 +    \<comment>\<open>Nonstandard definition\<close>
   17.42    "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
   17.43  
   17.44 -subsection {* Limits of Sequences *}
   17.45 +subsection \<open>Limits of Sequences\<close>
   17.46  
   17.47  lemma NSLIMSEQ_iff:
   17.48      "(X \<longlonglongrightarrow>\<^sub>N\<^sub>S L) = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
   17.49 @@ -102,7 +102,7 @@
   17.50  lemma NSLIMSEQ_norm: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S a \<Longrightarrow> (\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S norm a"
   17.51  by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)
   17.52  
   17.53 -text{*Uniqueness of limit*}
   17.54 +text\<open>Uniqueness of limit\<close>
   17.55  lemma NSLIMSEQ_unique: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S a; X \<longlonglongrightarrow>\<^sub>N\<^sub>S b |] ==> a = b"
   17.56  apply (simp add: NSLIMSEQ_def)
   17.57  apply (drule HNatInfinite_whn [THEN [2] bspec])+
   17.58 @@ -116,8 +116,8 @@
   17.59  apply (auto simp add: power_Suc intro: NSLIMSEQ_mult NSLIMSEQ_const)
   17.60  done
   17.61  
   17.62 -text{*We can now try and derive a few properties of sequences,
   17.63 -     starting with the limit comparison property for sequences.*}
   17.64 +text\<open>We can now try and derive a few properties of sequences,
   17.65 +     starting with the limit comparison property for sequences.\<close>
   17.66  
   17.67  lemma NSLIMSEQ_le:
   17.68         "[| f \<longlonglongrightarrow>\<^sub>N\<^sub>S l; g \<longlonglongrightarrow>\<^sub>N\<^sub>S m;
   17.69 @@ -138,9 +138,9 @@
   17.70  lemma NSLIMSEQ_le_const2: "[| X \<longlonglongrightarrow>\<^sub>N\<^sub>S (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
   17.71  by (erule NSLIMSEQ_le [OF _ NSLIMSEQ_const], auto)
   17.72  
   17.73 -text{*Shift a convergent series by 1:
   17.74 +text\<open>Shift a convergent series by 1:
   17.75    By the equivalence between Cauchiness and convergence and because
   17.76 -  the successor of an infinite hypernatural is also infinite.*}
   17.77 +  the successor of an infinite hypernatural is also infinite.\<close>
   17.78  
   17.79  lemma NSLIMSEQ_Suc: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S l ==> (%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l"
   17.80  apply (unfold NSLIMSEQ_def, safe)
   17.81 @@ -159,7 +159,7 @@
   17.82  lemma NSLIMSEQ_Suc_iff: "((%n. f(Suc n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S l) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S l)"
   17.83  by (blast intro: NSLIMSEQ_imp_Suc NSLIMSEQ_Suc)
   17.84  
   17.85 -subsubsection {* Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ} *}
   17.86 +subsubsection \<open>Equivalence of @{term LIMSEQ} and @{term NSLIMSEQ}\<close>
   17.87  
   17.88  lemma LIMSEQ_NSLIMSEQ:
   17.89    assumes X: "X \<longlonglongrightarrow> L" shows "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L"
   17.90 @@ -202,17 +202,17 @@
   17.91  theorem LIMSEQ_NSLIMSEQ_iff: "(f \<longlonglongrightarrow> L) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
   17.92  by (blast intro: LIMSEQ_NSLIMSEQ NSLIMSEQ_LIMSEQ)
   17.93  
   17.94 -subsubsection {* Derived theorems about @{term NSLIMSEQ} *}
   17.95 +subsubsection \<open>Derived theorems about @{term NSLIMSEQ}\<close>
   17.96  
   17.97 -text{*We prove the NS version from the standard one, since the NS proof
   17.98 -   seems more complicated than the standard one above!*}
   17.99 +text\<open>We prove the NS version from the standard one, since the NS proof
  17.100 +   seems more complicated than the standard one above!\<close>
  17.101  lemma NSLIMSEQ_norm_zero: "((\<lambda>n. norm (X n)) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (X \<longlonglongrightarrow>\<^sub>N\<^sub>S 0)"
  17.102  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_norm_zero_iff)
  17.103  
  17.104  lemma NSLIMSEQ_rabs_zero: "((%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0) = (f \<longlonglongrightarrow>\<^sub>N\<^sub>S (0::real))"
  17.105  by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] tendsto_rabs_zero_iff)
  17.106  
  17.107 -text{*Generalization to other limits*}
  17.108 +text\<open>Generalization to other limits\<close>
  17.109  lemma NSLIMSEQ_imp_rabs: "f \<longlonglongrightarrow>\<^sub>N\<^sub>S (l::real) ==> (%n. \<bar>f n\<bar>) \<longlonglongrightarrow>\<^sub>N\<^sub>S \<bar>l\<bar>"
  17.110  apply (simp add: NSLIMSEQ_def)
  17.111  apply (auto intro: approx_hrabs 
  17.112 @@ -240,7 +240,7 @@
  17.113    using LIMSEQ_inverse_real_of_nat_add_minus_mult by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric])
  17.114  
  17.115  
  17.116 -subsection {* Convergence *}
  17.117 +subsection \<open>Convergence\<close>
  17.118  
  17.119  lemma nslimI: "X \<longlonglongrightarrow>\<^sub>N\<^sub>S L ==> nslim X = L"
  17.120  apply (simp add: nslim_def)
  17.121 @@ -263,7 +263,7 @@
  17.122  by (auto intro: theI NSLIMSEQ_unique simp add: NSconvergent_def nslim_def)
  17.123  
  17.124  
  17.125 -subsection {* Bounded Monotonic Sequences *}
  17.126 +subsection \<open>Bounded Monotonic Sequences\<close>
  17.127  
  17.128  lemma NSBseqD: "[| NSBseq X;  N: HNatInfinite |] ==> ( *f* X) N : HFinite"
  17.129  by (simp add: NSBseq_def)
  17.130 @@ -281,7 +281,7 @@
  17.131  lemma NSBseqI: "\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite ==> NSBseq X"
  17.132  by (simp add: NSBseq_def)
  17.133  
  17.134 -text{*The standard definition implies the nonstandard definition*}
  17.135 +text\<open>The standard definition implies the nonstandard definition\<close>
  17.136  
  17.137  lemma Bseq_NSBseq: "Bseq X ==> NSBseq X"
  17.138  proof (unfold NSBseq_def, safe)
  17.139 @@ -295,7 +295,7 @@
  17.140    thus "starfun X N \<in> HFinite" by (simp add: HFinite_def)
  17.141  qed
  17.142  
  17.143 -text{*The nonstandard definition implies the standard definition*}
  17.144 +text\<open>The nonstandard definition implies the standard definition\<close>
  17.145  
  17.146  lemma SReal_less_omega: "r \<in> \<real> \<Longrightarrow> r < \<omega>"
  17.147  apply (insert HInfinite_omega)
  17.148 @@ -326,27 +326,27 @@
  17.149      by (simp add: HFinite_HInfinite_iff)
  17.150  qed
  17.151  
  17.152 -text{* Equivalence of nonstandard and standard definitions
  17.153 -  for a bounded sequence*}
  17.154 +text\<open>Equivalence of nonstandard and standard definitions
  17.155 +  for a bounded sequence\<close>
  17.156  lemma Bseq_NSBseq_iff: "(Bseq X) = (NSBseq X)"
  17.157  by (blast intro!: NSBseq_Bseq Bseq_NSBseq)
  17.158  
  17.159 -text{*A convergent sequence is bounded: 
  17.160 +text\<open>A convergent sequence is bounded: 
  17.161   Boundedness as a necessary condition for convergence. 
  17.162 - The nonstandard version has no existential, as usual *}
  17.163 + The nonstandard version has no existential, as usual\<close>
  17.164  
  17.165  lemma NSconvergent_NSBseq: "NSconvergent X ==> NSBseq X"
  17.166  apply (simp add: NSconvergent_def NSBseq_def NSLIMSEQ_def)
  17.167  apply (blast intro: HFinite_star_of approx_sym approx_HFinite)
  17.168  done
  17.169  
  17.170 -text{*Standard Version: easily now proved using equivalence of NS and
  17.171 - standard definitions *}
  17.172 +text\<open>Standard Version: easily now proved using equivalence of NS and
  17.173 + standard definitions\<close>
  17.174  
  17.175  lemma convergent_Bseq: "convergent X ==> Bseq (X::nat \<Rightarrow> _::real_normed_vector)"
  17.176  by (simp add: NSconvergent_NSBseq convergent_NSconvergent_iff Bseq_NSBseq_iff)
  17.177  
  17.178 -subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
  17.179 +subsubsection\<open>Upper Bounds and Lubs of Bounded Sequences\<close>
  17.180  
  17.181  lemma NSBseq_isUb: "NSBseq X ==> \<exists>U::real. isUb UNIV {x. \<exists>n. X n = x} U"
  17.182  by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isUb)
  17.183 @@ -354,11 +354,11 @@
  17.184  lemma NSBseq_isLub: "NSBseq X ==> \<exists>U::real. isLub UNIV {x. \<exists>n. X n = x} U"
  17.185  by (simp add: Bseq_NSBseq_iff [symmetric] Bseq_isLub)
  17.186  
  17.187 -subsubsection{*A Bounded and Monotonic Sequence Converges*}
  17.188 +subsubsection\<open>A Bounded and Monotonic Sequence Converges\<close>
  17.189  
  17.190 -text{* The best of both worlds: Easier to prove this result as a standard
  17.191 +text\<open>The best of both worlds: Easier to prove this result as a standard
  17.192     theorem and then use equivalence to "transfer" it into the
  17.193 -   equivalent nonstandard form if needed!*}
  17.194 +   equivalent nonstandard form if needed!\<close>
  17.195  
  17.196  lemma Bmonoseq_NSLIMSEQ: "\<forall>n \<ge> m. X n = X m ==> \<exists>L. (X \<longlonglongrightarrow>\<^sub>N\<^sub>S L)"
  17.197  by (auto dest!: Bmonoseq_LIMSEQ simp add: LIMSEQ_NSLIMSEQ_iff)
  17.198 @@ -370,7 +370,7 @@
  17.199                     Bseq_NSBseq_iff [symmetric])
  17.200  
  17.201  
  17.202 -subsection {* Cauchy Sequences *}
  17.203 +subsection \<open>Cauchy Sequences\<close>
  17.204  
  17.205  lemma NSCauchyI:
  17.206    "(\<And>M N. \<lbrakk>M \<in> HNatInfinite; N \<in> HNatInfinite\<rbrakk> \<Longrightarrow> starfun X M \<approx> starfun X N)
  17.207 @@ -382,7 +382,7 @@
  17.208     \<Longrightarrow> starfun X M \<approx> starfun X N"
  17.209  by (simp add: NSCauchy_def)
  17.210  
  17.211 -subsubsection{*Equivalence Between NS and Standard*}
  17.212 +subsubsection\<open>Equivalence Between NS and Standard\<close>
  17.213  
  17.214  lemma Cauchy_NSCauchy:
  17.215    assumes X: "Cauchy X" shows "NSCauchy X"
  17.216 @@ -430,16 +430,16 @@
  17.217  theorem NSCauchy_Cauchy_iff: "NSCauchy X = Cauchy X"
  17.218  by (blast intro!: NSCauchy_Cauchy Cauchy_NSCauchy)
  17.219  
  17.220 -subsubsection {* Cauchy Sequences are Bounded *}
  17.221 +subsubsection \<open>Cauchy Sequences are Bounded\<close>
  17.222  
  17.223 -text{*A Cauchy sequence is bounded -- nonstandard version*}
  17.224 +text\<open>A Cauchy sequence is bounded -- nonstandard version\<close>
  17.225  
  17.226  lemma NSCauchy_NSBseq: "NSCauchy X ==> NSBseq X"
  17.227  by (simp add: Cauchy_Bseq Bseq_NSBseq_iff [symmetric] NSCauchy_Cauchy_iff)
  17.228  
  17.229 -subsubsection {* Cauchy Sequences are Convergent *}
  17.230 +subsubsection \<open>Cauchy Sequences are Convergent\<close>
  17.231  
  17.232 -text{*Equivalence of Cauchy criterion and convergence:
  17.233 +text\<open>Equivalence of Cauchy criterion and convergence:
  17.234    We will prove this using our NS formulation which provides a
  17.235    much easier proof than using the standard definition. We do not
  17.236    need to use properties of subsequences such as boundedness,
  17.237 @@ -447,7 +447,7 @@
  17.238    in HOL which is much longer and more complicated. Of course, we do
  17.239    not have problems which he encountered with guessing the right
  17.240    instantiations for his 'espsilon-delta' proof(s) in this case
  17.241 -  since the NS formulations do not involve existential quantifiers.*}
  17.242 +  since the NS formulations do not involve existential quantifiers.\<close>
  17.243  
  17.244  lemma NSconvergent_NSCauchy: "NSconvergent X \<Longrightarrow> NSCauchy X"
  17.245  apply (simp add: NSconvergent_def NSLIMSEQ_def NSCauchy_def, safe)
  17.246 @@ -479,13 +479,13 @@
  17.247  by (fast intro: NSCauchy_NSconvergent NSconvergent_NSCauchy)
  17.248  
  17.249  
  17.250 -subsection {* Power Sequences *}
  17.251 +subsection \<open>Power Sequences\<close>
  17.252  
  17.253 -text{*The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
  17.254 +text\<open>The sequence @{term "x^n"} tends to 0 if @{term "0\<le>x"} and @{term
  17.255  "x<1"}.  Proof will use (NS) Cauchy equivalence for convergence and
  17.256 -  also fact that bounded and monotonic sequence converges.*}
  17.257 +  also fact that bounded and monotonic sequence converges.\<close>
  17.258  
  17.259 -text{* We now use NS criterion to bring proof of theorem through *}
  17.260 +text\<open>We now use NS criterion to bring proof of theorem through\<close>
  17.261  
  17.262  lemma NSLIMSEQ_realpow_zero:
  17.263    "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
    18.1 --- a/src/HOL/NSA/HSeries.thy	Wed Dec 30 11:32:56 2015 +0100
    18.2 +++ b/src/HOL/NSA/HSeries.thy	Wed Dec 30 11:37:29 2015 +0100
    18.3 @@ -5,7 +5,7 @@
    18.4  Converted to Isar and polished by lcp
    18.5  *)
    18.6  
    18.7 -section{*Finite Summation and Infinite Series for Hyperreals*}
    18.8 +section\<open>Finite Summation and Infinite Series for Hyperreals\<close>
    18.9  
   18.10  theory HSeries
   18.11  imports HSEQ
   18.12 @@ -31,11 +31,11 @@
   18.13  lemma sumhr_app: "sumhr(M,N,f) = ( *f2* (\<lambda>m n. setsum f {m..<n})) M N"
   18.14  by (simp add: sumhr_def)
   18.15  
   18.16 -text{*Base case in definition of @{term sumr}*}
   18.17 +text\<open>Base case in definition of @{term sumr}\<close>
   18.18  lemma sumhr_zero [simp]: "!!m. sumhr (m,0,f) = 0"
   18.19  unfolding sumhr_app by transfer simp
   18.20  
   18.21 -text{*Recursive case in definition of @{term sumr}*}
   18.22 +text\<open>Recursive case in definition of @{term sumr}\<close>
   18.23  lemma sumhr_if:
   18.24       "!!m n. sumhr(m,n+1,f) =
   18.25        (if n + 1 \<le> m then 0 else sumhr(m,n,f) + ( *f* f) n)"
   18.26 @@ -71,7 +71,7 @@
   18.27  lemma sumhr_hrabs: "!!m n. \<bar>sumhr(m,n,f)\<bar> \<le> sumhr(m,n,%i. \<bar>f i\<bar>)"
   18.28  unfolding sumhr_app by transfer (rule setsum_abs)
   18.29  
   18.30 -text{* other general version also needed *}
   18.31 +text\<open>other general version also needed\<close>
   18.32  lemma sumhr_fun_hypnat_eq:
   18.33     "(\<forall>r. m \<le> r & r < n --> f r = g r) -->
   18.34        sumhr(hypnat_of_nat m, hypnat_of_nat n, f) =
   18.35 @@ -94,10 +94,10 @@
   18.36  unfolding sumhr_app by transfer (rule setsum_shift_bounds_nat_ivl)
   18.37  
   18.38  
   18.39 -subsection{*Nonstandard Sums*}
   18.40 +subsection\<open>Nonstandard Sums\<close>
   18.41  
   18.42 -text{*Infinite sums are obtained by summing to some infinite hypernatural
   18.43 - (such as @{term whn})*}
   18.44 +text\<open>Infinite sums are obtained by summing to some infinite hypernatural
   18.45 + (such as @{term whn})\<close>
   18.46  lemma sumhr_hypreal_of_hypnat_omega:
   18.47        "sumhr(0,whn,%i. 1) = hypreal_of_hypnat whn"
   18.48  by (simp add: sumhr_const)
   18.49 @@ -179,7 +179,7 @@
   18.50              simp add: sumhr_split_diff atLeast0LessThan[symmetric])
   18.51  done
   18.52  
   18.53 -text{*Terms of a convergent series tend to zero*}
   18.54 +text\<open>Terms of a convergent series tend to zero\<close>
   18.55  lemma NSsummable_NSLIMSEQ_zero: "NSsummable f ==> f \<longlonglongrightarrow>\<^sub>N\<^sub>S 0"
   18.56  apply (auto simp add: NSLIMSEQ_def NSsummable_NSCauchy)
   18.57  apply (drule bspec, auto)
   18.58 @@ -187,7 +187,7 @@
   18.59  apply (auto intro: HNatInfinite_add_one approx_hrabs_zero_cancel)
   18.60  done
   18.61  
   18.62 -text{*Nonstandard comparison test*}
   18.63 +text\<open>Nonstandard comparison test\<close>
   18.64  lemma NSsummable_comparison_test:
   18.65       "[| \<exists>N. \<forall>n. N \<le> n --> \<bar>f n\<bar> \<le> g n; NSsummable g |] ==> NSsummable f"
   18.66  apply (fold summable_NSsummable_iff)
    19.1 --- a/src/HOL/NSA/HTranscendental.thy	Wed Dec 30 11:32:56 2015 +0100
    19.2 +++ b/src/HOL/NSA/HTranscendental.thy	Wed Dec 30 11:37:29 2015 +0100
    19.3 @@ -5,7 +5,7 @@
    19.4  Converted to Isar and polished by lcp
    19.5  *)
    19.6  
    19.7 -section{*Nonstandard Extensions of Transcendental Functions*}
    19.8 +section\<open>Nonstandard Extensions of Transcendental Functions\<close>
    19.9  
   19.10  theory HTranscendental
   19.11  imports Transcendental HSeries HDeriv
   19.12 @@ -13,7 +13,7 @@
   19.13  
   19.14  definition
   19.15    exphr :: "real => hypreal" where
   19.16 -    --{*define exponential function using standard part *}
   19.17 +    \<comment>\<open>define exponential function using standard part\<close>
   19.18    "exphr x =  st(sumhr (0, whn, %n. inverse (fact n) * (x ^ n)))"
   19.19  
   19.20  definition
   19.21 @@ -25,7 +25,7 @@
   19.22    "coshr x = st(sumhr (0, whn, %n. cos_coeff n * x ^ n))"
   19.23  
   19.24  
   19.25 -subsection{*Nonstandard Extension of Square Root Function*}
   19.26 +subsection\<open>Nonstandard Extension of Square Root Function\<close>
   19.27  
   19.28  lemma STAR_sqrt_zero [simp]: "( *f* sqrt) 0 = 0"
   19.29  by (simp add: starfun star_n_zero_num)
   19.30 @@ -592,7 +592,7 @@
   19.31  by (insert NSLIMSEQ_mult [OF NSLIMSEQ_sin_pi NSLIMSEQ_cos_one], simp)
   19.32  
   19.33  
   19.34 -text{*A familiar approximation to @{term "cos x"} when @{term x} is small*}
   19.35 +text\<open>A familiar approximation to @{term "cos x"} when @{term x} is small\<close>
   19.36  
   19.37  lemma STAR_cos_Infinitesimal_approx:
   19.38    fixes x :: "'a::{real_normed_field,banach} star"
   19.39 @@ -603,7 +603,7 @@
   19.40  done
   19.41  
   19.42  lemma STAR_cos_Infinitesimal_approx2:
   19.43 -  fixes x :: hypreal  --{*perhaps could be generalised, like many other hypreal results*}
   19.44 +  fixes x :: hypreal  \<comment>\<open>perhaps could be generalised, like many other hypreal results\<close>
   19.45    shows "x \<in> Infinitesimal ==> ( *f* cos) x @= 1 - (x\<^sup>2)/2"
   19.46  apply (rule STAR_cos_Infinitesimal [THEN approx_trans])
   19.47  apply (auto intro: Infinitesimal_SReal_divide Infinitesimal_mult
    20.1 --- a/src/HOL/NSA/HyperDef.thy	Wed Dec 30 11:32:56 2015 +0100
    20.2 +++ b/src/HOL/NSA/HyperDef.thy	Wed Dec 30 11:37:29 2015 +0100
    20.3 @@ -4,7 +4,7 @@
    20.4      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    20.5  *)
    20.6  
    20.7 -section{*Construction of Hyperreals Using Ultrafilters*}
    20.8 +section\<open>Construction of Hyperreals Using Ultrafilters\<close>
    20.9  
   20.10  theory HyperDef
   20.11  imports Complex_Main HyperNat
   20.12 @@ -22,12 +22,12 @@
   20.13  
   20.14  definition
   20.15    omega :: hypreal where
   20.16 -   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
   20.17 +   \<comment> \<open>an infinite number \<open>= [<1,2,3,...>]\<close>\<close>
   20.18    "omega = star_n (\<lambda>n. real (Suc n))"
   20.19  
   20.20  definition
   20.21    epsilon :: hypreal where
   20.22 -   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
   20.23 +   \<comment> \<open>an infinitesimal number \<open>= [<1,1/2,1/3,...>]\<close>\<close>
   20.24    "epsilon = star_n (\<lambda>n. inverse (real (Suc n)))"
   20.25  
   20.26  notation (xsymbols)
   20.27 @@ -35,7 +35,7 @@
   20.28    epsilon  ("\<epsilon>")
   20.29  
   20.30  
   20.31 -subsection {* Real vector class instances *}
   20.32 +subsection \<open>Real vector class instances\<close>
   20.33  
   20.34  instantiation star :: (scaleR) scaleR
   20.35  begin
   20.36 @@ -103,7 +103,7 @@
   20.37  by (simp add: Reals_def Standard_def)
   20.38  
   20.39  
   20.40 -subsection {* Injection from @{typ hypreal} *}
   20.41 +subsection \<open>Injection from @{typ hypreal}\<close>
   20.42  
   20.43  definition
   20.44    of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
   20.45 @@ -153,7 +153,7 @@
   20.46  by transfer (rule of_real_eq_0_iff)
   20.47  
   20.48  
   20.49 -subsection{*Properties of @{term starrel}*}
   20.50 +subsection\<open>Properties of @{term starrel}\<close>
   20.51  
   20.52  lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"
   20.53  by (simp add: starrel_def)
   20.54 @@ -164,8 +164,8 @@
   20.55  declare Abs_star_inject [simp] Abs_star_inverse [simp]
   20.56  declare equiv_starrel [THEN eq_equiv_class_iff, simp]
   20.57  
   20.58 -subsection{*@{term hypreal_of_real}:
   20.59 -            the Injection from @{typ real} to @{typ hypreal}*}
   20.60 +subsection\<open>@{term hypreal_of_real}:
   20.61 +            the Injection from @{typ real} to @{typ hypreal}\<close>
   20.62  
   20.63  lemma inj_star_of: "inj star_of"
   20.64  by (rule inj_onI, simp)
   20.65 @@ -180,7 +180,7 @@
   20.66  lemma Rep_star_star_n: "X \<in> Rep_star (star_n X)"
   20.67  by simp
   20.68  
   20.69 -subsection{* Properties of @{term star_n} *}
   20.70 +subsection\<open>Properties of @{term star_n}\<close>
   20.71  
   20.72  lemma star_n_add:
   20.73    "star_n X + star_n Y = star_n (%n. X n + Y n)"
   20.74 @@ -222,13 +222,13 @@
   20.75  lemma hypreal_omega_gt_zero [simp]: "0 < omega"
   20.76  by (simp add: omega_def star_n_zero_num star_n_less)
   20.77  
   20.78 -subsection{*Existence of Infinite Hyperreal Number*}
   20.79 +subsection\<open>Existence of Infinite Hyperreal Number\<close>
   20.80  
   20.81 -text{*Existence of infinite number not corresponding to any real number.
   20.82 -Use assumption that member @{term FreeUltrafilterNat} is not finite.*}
   20.83 +text\<open>Existence of infinite number not corresponding to any real number.
   20.84 +Use assumption that member @{term FreeUltrafilterNat} is not finite.\<close>
   20.85  
   20.86  
   20.87 -text{*A few lemmas first*}
   20.88 +text\<open>A few lemmas first\<close>
   20.89  
   20.90  lemma lemma_omega_empty_singleton_disj:
   20.91    "{n::nat. x = real n} = {} \<or> (\<exists>y. {n::nat. x = real n} = {y})"
   20.92 @@ -249,8 +249,8 @@
   20.93  lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega"
   20.94  by (insert not_ex_hypreal_of_real_eq_omega, auto)
   20.95  
   20.96 -text{*Existence of infinitesimal number also not corresponding to any
   20.97 - real number*}
   20.98 +text\<open>Existence of infinitesimal number also not corresponding to any
   20.99 + real number\<close>
  20.100  
  20.101  lemma lemma_epsilon_empty_singleton_disj:
  20.102       "{n::nat. x = inverse(real(Suc n))} = {} |
  20.103 @@ -277,7 +277,7 @@
  20.104  lemma hypreal_epsilon_gt_zero: "0 < epsilon"
  20.105  by (simp add: hypreal_epsilon_inverse_omega)
  20.106  
  20.107 -subsection{*Absolute Value Function for the Hyperreals*}
  20.108 +subsection\<open>Absolute Value Function for the Hyperreals\<close>
  20.109  
  20.110  lemma hrabs_add_less: "[| \<bar>x\<bar> < r; \<bar>y\<bar> < s |] ==> \<bar>x + y\<bar> < r + (s::hypreal)"
  20.111  by (simp add: abs_if split: split_if_asm)
  20.112 @@ -292,7 +292,7 @@
  20.113  by (simp add: abs_if split add: split_if_asm)
  20.114  
  20.115  
  20.116 -subsection{*Embedding the Naturals into the Hyperreals*}
  20.117 +subsection\<open>Embedding the Naturals into the Hyperreals\<close>
  20.118  
  20.119  abbreviation
  20.120    hypreal_of_nat :: "nat => hypreal" where
  20.121 @@ -309,20 +309,20 @@
  20.122  lemma hypreal_of_nat: "hypreal_of_nat m = star_n (%n. real m)"
  20.123  by (simp add: star_of_def [symmetric])
  20.124  
  20.125 -declaration {*
  20.126 +declaration \<open>
  20.127    K (Lin_Arith.add_inj_thms [@{thm star_of_le} RS iffD2,
  20.128      @{thm star_of_less} RS iffD2, @{thm star_of_eq} RS iffD2]
  20.129    #> Lin_Arith.add_simps [@{thm star_of_zero}, @{thm star_of_one},
  20.130        @{thm star_of_numeral}, @{thm star_of_add},
  20.131        @{thm star_of_minus}, @{thm star_of_diff}, @{thm star_of_mult}]
  20.132    #> Lin_Arith.add_inj_const (@{const_name "StarDef.star_of"}, @{typ "real \<Rightarrow> hypreal"}))
  20.133 -*}
  20.134 +\<close>
  20.135  
  20.136  simproc_setup fast_arith_hypreal ("(m::hypreal) < n" | "(m::hypreal) <= n" | "(m::hypreal) = n") =
  20.137 -  {* K Lin_Arith.simproc *}
  20.138 +  \<open>K Lin_Arith.simproc\<close>
  20.139  
  20.140  
  20.141 -subsection {* Exponentials on the Hyperreals *}
  20.142 +subsection \<open>Exponentials on the Hyperreals\<close>
  20.143  
  20.144  lemma hpowr_0 [simp]:   "r ^ 0       = (1::hypreal)"
  20.145  by (rule power_0)
  20.146 @@ -349,7 +349,7 @@
  20.147  by arith
  20.148  
  20.149  
  20.150 -text{*FIXME: DELETE THESE*}
  20.151 +text\<open>FIXME: DELETE THESE\<close>
  20.152  lemma hypreal_three_squares_add_zero_iff:
  20.153       "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
  20.154  apply (simp only: zero_le_square add_nonneg_nonneg hypreal_add_nonneg_eq_0_iff, auto)
  20.155 @@ -397,7 +397,7 @@
  20.156  done
  20.157  *)
  20.158  
  20.159 -subsection{*Powers with Hypernatural Exponents*}
  20.160 +subsection\<open>Powers with Hypernatural Exponents\<close>
  20.161  
  20.162  definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
  20.163    hyperpow_def [transfer_unfold]: "R pow N = ( *f2* op ^) R N"
  20.164 @@ -478,7 +478,7 @@
  20.165    "\<bar>x::'a::{linordered_idom} star\<bar> pow 2 = x pow 2"
  20.166  by (simp add: hyperpow_hrabs)
  20.167  
  20.168 -text{*The precondition could be weakened to @{term "0\<le>x"}*}
  20.169 +text\<open>The precondition could be weakened to @{term "0\<le>x"}\<close>
  20.170  lemma hypreal_mult_less_mono:
  20.171       "[| u<v;  x<y;  (0::hypreal) < v;  0 < x |] ==> u*x < v* y"
  20.172   by (simp add: mult_strict_mono order_less_imp_le)
    21.1 --- a/src/HOL/NSA/HyperNat.thy	Wed Dec 30 11:32:56 2015 +0100
    21.2 +++ b/src/HOL/NSA/HyperNat.thy	Wed Dec 30 11:37:29 2015 +0100
    21.3 @@ -5,7 +5,7 @@
    21.4  Converted to Isar and polished by lcp    
    21.5  *)
    21.6  
    21.7 -section{*Hypernatural numbers*}
    21.8 +section\<open>Hypernatural numbers\<close>
    21.9  
   21.10  theory HyperNat
   21.11  imports StarDef
   21.12 @@ -21,7 +21,7 @@
   21.13    hSuc :: "hypnat => hypnat" where
   21.14    hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
   21.15  
   21.16 -subsection{*Properties Transferred from Naturals*}
   21.17 +subsection\<open>Properties Transferred from Naturals\<close>
   21.18  
   21.19  lemma hSuc_not_zero [iff]: "\<And>m. hSuc m \<noteq> 0"
   21.20  by transfer (rule Suc_not_Zero)
   21.21 @@ -128,7 +128,7 @@
   21.22  
   21.23  lemma hypnat_diff_split:
   21.24      "P(a - b::hypnat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
   21.25 -    -- {* elimination of @{text -} on @{text hypnat} *}
   21.26 +    \<comment> \<open>elimination of \<open>-\<close> on \<open>hypnat\<close>\<close>
   21.27  proof (cases "a<b" rule: case_split)
   21.28    case True
   21.29      thus ?thesis
   21.30 @@ -140,7 +140,7 @@
   21.31        by (auto simp add: linorder_not_less dest: order_le_less_trans) 
   21.32  qed
   21.33  
   21.34 -subsection{*Properties of the set of embedded natural numbers*}
   21.35 +subsection\<open>Properties of the set of embedded natural numbers\<close>
   21.36  
   21.37  lemma of_nat_eq_star_of [simp]: "of_nat = star_of"
   21.38  proof
   21.39 @@ -173,7 +173,7 @@
   21.40  by (simp add: Nats_eq_Standard)
   21.41  
   21.42  
   21.43 -subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}
   21.44 +subsection\<open>Infinite Hypernatural Numbers -- @{term HNatInfinite}\<close>
   21.45  
   21.46  definition
   21.47    (* the set of infinite hypernatural numbers *)
   21.48 @@ -209,7 +209,7 @@
   21.49  lemma star_of_le_HNatInfinite: "N \<in> HNatInfinite \<Longrightarrow> star_of n \<le> N"
   21.50  by (rule star_of_less_HNatInfinite [THEN order_less_imp_le])
   21.51  
   21.52 -subsubsection {* Closure Rules *}
   21.53 +subsubsection \<open>Closure Rules\<close>
   21.54  
   21.55  lemma Nats_less_HNatInfinite: "\<lbrakk>x \<in> Nats; y \<in> HNatInfinite\<rbrakk> \<Longrightarrow> x < y"
   21.56  by (auto simp add: Nats_def star_of_less_HNatInfinite)
   21.57 @@ -266,7 +266,7 @@
   21.58  done
   21.59  
   21.60  
   21.61 -subsection{*Existence of an infinite hypernatural number*}
   21.62 +subsection\<open>Existence of an infinite hypernatural number\<close>
   21.63  
   21.64  definition
   21.65    (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
   21.66 @@ -315,9 +315,9 @@
   21.67  by (simp add: Nats_less_whn)
   21.68  
   21.69  
   21.70 -subsubsection{*Alternative characterization of the set of infinite hypernaturals*}
   21.71 +subsubsection\<open>Alternative characterization of the set of infinite hypernaturals\<close>
   21.72  
   21.73 -text{* @{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
   21.74 +text\<open>@{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}\<close>
   21.75  
   21.76  (*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
   21.77  lemma HNatInfinite_FreeUltrafilterNat_lemma:
   21.78 @@ -337,8 +337,8 @@
   21.79  done
   21.80  
   21.81  
   21.82 -subsubsection{*Alternative Characterization of @{term HNatInfinite} using 
   21.83 -Free Ultrafilter*}
   21.84 +subsubsection\<open>Alternative Characterization of @{term HNatInfinite} using 
   21.85 +Free Ultrafilter\<close>
   21.86  
   21.87  lemma HNatInfinite_FreeUltrafilterNat:
   21.88       "star_n X \<in> HNatInfinite ==> \<forall>u. eventually (\<lambda>n. u < X n) FreeUltrafilterNat"
   21.89 @@ -356,7 +356,7 @@
   21.90  by (rule iffI [OF HNatInfinite_FreeUltrafilterNat 
   21.91                   FreeUltrafilterNat_HNatInfinite])
   21.92  
   21.93 -subsection {* Embedding of the Hypernaturals into other types *}
   21.94 +subsection \<open>Embedding of the Hypernaturals into other types\<close>
   21.95  
   21.96  definition
   21.97    of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
    22.1 --- a/src/HOL/NSA/NSA.thy	Wed Dec 30 11:32:56 2015 +0100
    22.2 +++ b/src/HOL/NSA/NSA.thy	Wed Dec 30 11:37:29 2015 +0100
    22.3 @@ -3,7 +3,7 @@
    22.4      Author:     Lawrence C Paulson, University of Cambridge
    22.5  *)
    22.6  
    22.7 -section{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
    22.8 +section\<open>Infinite Numbers, Infinitesimals, Infinitely Close Relation\<close>
    22.9  
   22.10  theory NSA
   22.11  imports HyperDef "~~/src/HOL/Library/Lub_Glb"
   22.12 @@ -27,12 +27,12 @@
   22.13  
   22.14  definition
   22.15    approx :: "['a::real_normed_vector star, 'a star] => bool"  (infixl "@=" 50) where
   22.16 -    --{*the `infinitely close' relation*}
   22.17 +    \<comment>\<open>the `infinitely close' relation\<close>
   22.18    "(x @= y) = ((x - y) \<in> Infinitesimal)"
   22.19  
   22.20  definition
   22.21    st        :: "hypreal => hypreal" where
   22.22 -    --{*the standard part of a hyperreal*}
   22.23 +    \<comment>\<open>the standard part of a hyperreal\<close>
   22.24    "st = (%x. @r. x \<in> HFinite & r \<in> \<real> & r @= x)"
   22.25  
   22.26  definition
   22.27 @@ -49,7 +49,7 @@
   22.28  lemma SReal_def: "\<real> == {x. \<exists>r. x = hypreal_of_real r}"
   22.29  by (simp add: Reals_def image_def)
   22.30  
   22.31 -subsection {* Nonstandard Extension of the Norm Function *}
   22.32 +subsection \<open>Nonstandard Extension of the Norm Function\<close>
   22.33  
   22.34  definition
   22.35    scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
   22.36 @@ -171,7 +171,7 @@
   22.37  apply (simp add: mult_strict_mono')
   22.38  done
   22.39  
   22.40 -subsection{*Closure Laws for the Standard Reals*}
   22.41 +subsection\<open>Closure Laws for the Standard Reals\<close>
   22.42  
   22.43  lemma Reals_minus_iff [simp]: "(-x \<in> \<real>) = (x \<in> \<real>)"
   22.44  apply auto
   22.45 @@ -190,7 +190,7 @@
   22.46  lemma SReal_divide_numeral: "r \<in> \<real> ==> r/(numeral w::hypreal) \<in> \<real>"
   22.47  by simp
   22.48  
   22.49 -text{*epsilon is not in Reals because it is an infinitesimal*}
   22.50 +text\<open>epsilon is not in Reals because it is an infinitesimal\<close>
   22.51  lemma SReal_epsilon_not_mem: "epsilon \<notin> \<real>"
   22.52  apply (simp add: SReal_def)
   22.53  apply (auto simp add: hypreal_of_real_not_eq_epsilon [THEN not_sym])
   22.54 @@ -225,7 +225,7 @@
   22.55  apply (drule dense, auto)
   22.56  done
   22.57  
   22.58 -text{*Completeness of Reals, but both lemmas are unused.*}
   22.59 +text\<open>Completeness of Reals, but both lemmas are unused.\<close>
   22.60  
   22.61  lemma SReal_sup_lemma:
   22.62       "P \<subseteq> \<real> ==> ((\<exists>x \<in> P. y < x) =
   22.63 @@ -244,7 +244,7 @@
   22.64  done
   22.65  
   22.66  
   22.67 -subsection{* Set of Finite Elements is a Subring of the Extended Reals*}
   22.68 +subsection\<open>Set of Finite Elements is a Subring of the Extended Reals\<close>
   22.69  
   22.70  lemma HFinite_add: "[|x \<in> HFinite; y \<in> HFinite|] ==> (x+y) \<in> HFinite"
   22.71  apply (simp add: HFinite_def)
   22.72 @@ -315,7 +315,7 @@
   22.73  done
   22.74  
   22.75  
   22.76 -subsection{* Set of Infinitesimals is a Subring of the Hyperreals*}
   22.77 +subsection\<open>Set of Infinitesimals is a Subring of the Hyperreals\<close>
   22.78  
   22.79  lemma InfinitesimalI:
   22.80    "(\<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> hnorm x < r) \<Longrightarrow> x \<in> Infinitesimal"
   22.81 @@ -609,7 +609,7 @@
   22.82  by (erule HFinite_star_of [THEN [2] Infinitesimal_HFinite_mult2])
   22.83  
   22.84  
   22.85 -subsection{*The Infinitely Close Relation*}
   22.86 +subsection\<open>The Infinitely Close Relation\<close>
   22.87  
   22.88  lemma mem_infmal_iff: "(x \<in> Infinitesimal) = (x @= 0)"
   22.89  by (simp add: Infinitesimal_def approx_def)
   22.90 @@ -651,7 +651,7 @@
   22.91    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
   22.92  simproc_setup approx_reorient_simproc
   22.93    ("0 @= x" | "1 @= y" | "numeral w @= z" | "- 1 @= y" | "- numeral w @= r") =
   22.94 -{*
   22.95 +\<open>
   22.96    let val rule = @{thm approx_reorient} RS eq_reflection
   22.97        fun proc phi ss ct =
   22.98          case Thm.term_of ct of
   22.99 @@ -659,7 +659,7 @@
  22.100              else if can HOLogic.dest_number t then SOME rule else NONE
  22.101          | _ => NONE
  22.102    in proc end
  22.103 -*}
  22.104 +\<close>
  22.105  
  22.106  lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"
  22.107  by (simp add: approx_minus_iff [symmetric] mem_infmal_iff)
  22.108 @@ -901,7 +901,7 @@
  22.109  qed
  22.110  
  22.111  
  22.112 -subsection{* Zero is the Only Infinitesimal that is also a Real*}
  22.113 +subsection\<open>Zero is the Only Infinitesimal that is also a Real\<close>
  22.114  
  22.115  lemma Infinitesimal_less_SReal:
  22.116       "[| (x::hypreal) \<in> \<real>; y \<in> Infinitesimal; 0 < x |] ==> y < x"
  22.117 @@ -1004,7 +1004,7 @@
  22.118         close to a unique real number (i.e a member of Reals)
  22.119   ------------------------------------------------------------------*)
  22.120  
  22.121 -subsection{* Uniqueness: Two Infinitely Close Reals are Equal*}
  22.122 +subsection\<open>Uniqueness: Two Infinitely Close Reals are Equal\<close>
  22.123  
  22.124  lemma star_of_approx_iff [simp]: "(star_of x @= star_of y) = (x = y)"
  22.125  apply safe
  22.126 @@ -1061,9 +1061,9 @@
  22.127  by (blast intro: SReal_approx_iff [THEN iffD1] approx_trans2)
  22.128  
  22.129  
  22.130 -subsection{* Existence of Unique Real Infinitely Close*}
  22.131 +subsection\<open>Existence of Unique Real Infinitely Close\<close>
  22.132  
  22.133 -subsubsection{*Lifting of the Ub and Lub Properties*}
  22.134 +subsubsection\<open>Lifting of the Ub and Lub Properties\<close>
  22.135  
  22.136  lemma hypreal_of_real_isUb_iff:
  22.137        "(isUb \<real> (hypreal_of_real ` Q) (hypreal_of_real Y)) =
  22.138 @@ -1255,7 +1255,7 @@
  22.139  
  22.140  
  22.141  
  22.142 -text{*Existence of real and Standard Part Theorem*}
  22.143 +text\<open>Existence of real and Standard Part Theorem\<close>
  22.144  lemma lemma_st_part_Ex:
  22.145       "(x::hypreal) \<in> HFinite
  22.146         ==> \<exists>t \<in> Reals. \<forall>r \<in> Reals. 0 < r --> \<bar>x - t\<bar> < r"
  22.147 @@ -1270,14 +1270,14 @@
  22.148  apply (drule lemma_st_part_Ex, auto)
  22.149  done
  22.150  
  22.151 -text{*There is a unique real infinitely close*}
  22.152 +text\<open>There is a unique real infinitely close\<close>
  22.153  lemma st_part_Ex1: "x \<in> HFinite ==> EX! t::hypreal. t \<in> \<real> & x @= t"
  22.154  apply (drule st_part_Ex, safe)
  22.155  apply (drule_tac [2] approx_sym, drule_tac [2] approx_sym, drule_tac [2] approx_sym)
  22.156  apply (auto intro!: approx_unique_real)
  22.157  done
  22.158  
  22.159 -subsection{* Finite, Infinite and Infinitesimal*}
  22.160 +subsection\<open>Finite, Infinite and Infinitesimal\<close>
  22.161  
  22.162  lemma HFinite_Int_HInfinite_empty [simp]: "HFinite Int HInfinite = {}"
  22.163  apply (simp add: HFinite_def HInfinite_def)
  22.164 @@ -1487,7 +1487,7 @@
  22.165  by (cut_tac x = x in hrabs_disj, auto)
  22.166  
  22.167  
  22.168 -subsection{*Theorems about Monads*}
  22.169 +subsection\<open>Theorems about Monads\<close>
  22.170  
  22.171  lemma monad_hrabs_Un_subset: "monad \<bar>x\<bar> \<le> monad(x::hypreal) Un monad(-x)"
  22.172  by (rule_tac x1 = x in hrabs_disj [THEN disjE], auto)
  22.173 @@ -1514,7 +1514,7 @@
  22.174  by (simp add: monad_def)
  22.175  
  22.176  
  22.177 -subsection{*Proof that @{term "x @= y"} implies @{term"\<bar>x\<bar> @= \<bar>y\<bar>"}*}
  22.178 +subsection\<open>Proof that @{term "x @= y"} implies @{term"\<bar>x\<bar> @= \<bar>y\<bar>"}\<close>
  22.179  
  22.180  lemma approx_subset_monad: "x @= y ==> {x,y} \<le> monad x"
  22.181  apply (simp (no_asm))
  22.182 @@ -1609,7 +1609,7 @@
  22.183  apply (auto intro: approx_trans2)
  22.184  done
  22.185  
  22.186 -subsection {* More @{term HFinite} and @{term Infinitesimal} Theorems *}
  22.187 +subsection \<open>More @{term HFinite} and @{term Infinitesimal} Theorems\<close>
  22.188  
  22.189  (* interesting slightly counterintuitive theorem: necessary
  22.190     for proving that an open interval is an NS open set
  22.191 @@ -1753,7 +1753,7 @@
  22.192  done
  22.193  
  22.194  
  22.195 -subsection{* Theorems about Standard Part*}
  22.196 +subsection\<open>Theorems about Standard Part\<close>
  22.197  
  22.198  lemma st_approx_self: "x \<in> HFinite ==> st x @= x"
  22.199  apply (simp add: st_def)
  22.200 @@ -1909,9 +1909,9 @@
  22.201  
  22.202  
  22.203  
  22.204 -subsection {* Alternative Definitions using Free Ultrafilter *}
  22.205 +subsection \<open>Alternative Definitions using Free Ultrafilter\<close>
  22.206  
  22.207 -subsubsection {* @{term HFinite} *}
  22.208 +subsubsection \<open>@{term HFinite}\<close>
  22.209  
  22.210  lemma HFinite_FreeUltrafilterNat:
  22.211      "star_n X \<in> HFinite
  22.212 @@ -1936,7 +1936,7 @@
  22.213       "(star_n X \<in> HFinite) = (\<exists>u. eventually (\<lambda>n. norm (X n) < u) FreeUltrafilterNat)"
  22.214  by (blast intro!: HFinite_FreeUltrafilterNat FreeUltrafilterNat_HFinite)
  22.215  
  22.216 -subsubsection {* @{term HInfinite} *}
  22.217 +subsubsection \<open>@{term HInfinite}\<close>
  22.218  
  22.219  lemma lemma_Compl_eq: "- {n. u < norm (f n)} = {n. norm (f n) \<le> u}"
  22.220  by auto
  22.221 @@ -1996,7 +1996,7 @@
  22.222       "(star_n X \<in> HInfinite) = (\<forall>u. eventually (\<lambda>n. u < norm (X n)) FreeUltrafilterNat)"
  22.223  by (blast intro!: HInfinite_FreeUltrafilterNat FreeUltrafilterNat_HInfinite)
  22.224  
  22.225 -subsubsection {* @{term Infinitesimal} *}
  22.226 +subsubsection \<open>@{term Infinitesimal}\<close>
  22.227  
  22.228  lemma ball_SReal_eq: "(\<forall>x::hypreal \<in> Reals. P x) = (\<forall>x::real. P (star_of x))"
  22.229  by (unfold SReal_def, auto)
  22.230 @@ -2050,9 +2050,9 @@
  22.231  done
  22.232  
  22.233  
  22.234 -subsection{*Proof that @{term omega} is an infinite number*}
  22.235 +subsection\<open>Proof that @{term omega} is an infinite number\<close>
  22.236  
  22.237 -text{*It will follow that epsilon is an infinitesimal number.*}
  22.238 +text\<open>It will follow that epsilon is an infinitesimal number.\<close>
  22.239  
  22.240  lemma Suc_Un_eq: "{n. n < Suc m} = {n. n < m} Un {n. n = m}"
  22.241  by (auto simp add: less_Suc_eq)
  22.242 @@ -2100,7 +2100,7 @@
  22.243  lemma Compl_real_le_eq: "- {n::nat. real n \<le> u} = {n. u < real n}"
  22.244  by (auto dest!: order_le_less_trans simp add: linorder_not_le)
  22.245  
  22.246 -text{*@{term omega} is a member of @{term HInfinite}*}
  22.247 +text\<open>@{term omega} is a member of @{term HInfinite}\<close>
  22.248  
  22.249  theorem HInfinite_omega [simp]: "omega \<in> HInfinite"
  22.250  apply (simp add: omega_def)
  22.251 @@ -2176,21 +2176,21 @@
  22.252  by (drule inverse_real_of_posnat_ge_real_FreeUltrafilterNat)
  22.253     (simp add: FreeUltrafilterNat.eventually_not_iff not_le[symmetric])
  22.254  
  22.255 -text{* Example of an hypersequence (i.e. an extended standard sequence)
  22.256 +text\<open>Example of an hypersequence (i.e. an extended standard sequence)
  22.257     whose term with an hypernatural suffix is an infinitesimal i.e.
  22.258 -   the whn'nth term of the hypersequence is a member of Infinitesimal*}
  22.259 +   the whn'nth term of the hypersequence is a member of Infinitesimal\<close>
  22.260  
  22.261  lemma SEQ_Infinitesimal:
  22.262        "( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
  22.263  by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff
  22.264          FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc)
  22.265  
  22.266 -text{* Example where we get a hyperreal from a real sequence
  22.267 +text\<open>Example where we get a hyperreal from a real sequence
  22.268        for which a particular property holds. The theorem is
  22.269        used in proofs about equivalence of nonstandard and
  22.270        standard neighbourhoods. Also used for equivalence of
  22.271        nonstandard ans standard definitions of pointwise
  22.272 -      limit.*}
  22.273 +      limit.\<close>
  22.274  
  22.275  (*-----------------------------------------------------
  22.276      |X(n) - x| < 1/n ==> [<X n>] - hypreal_of_real x| \<in> Infinitesimal
    23.1 --- a/src/HOL/NSA/NSCA.thy	Wed Dec 30 11:32:56 2015 +0100
    23.2 +++ b/src/HOL/NSA/NSCA.thy	Wed Dec 30 11:37:29 2015 +0100
    23.3 @@ -3,7 +3,7 @@
    23.4      Copyright   : 2001,2002 University of Edinburgh
    23.5  *)
    23.6  
    23.7 -section{*Non-Standard Complex Analysis*}
    23.8 +section\<open>Non-Standard Complex Analysis\<close>
    23.9  
   23.10  theory NSCA
   23.11  imports NSComplex HTranscendental
   23.12 @@ -14,12 +14,12 @@
   23.13     SComplex  :: "hcomplex set" where
   23.14     "SComplex \<equiv> Standard"
   23.15  
   23.16 -definition --{* standard part map*}
   23.17 +definition \<comment>\<open>standard part map\<close>
   23.18    stc :: "hcomplex => hcomplex" where 
   23.19    "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
   23.20  
   23.21  
   23.22 -subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
   23.23 +subsection\<open>Closure Laws for SComplex, the Standard Complex Numbers\<close>
   23.24  
   23.25  lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"
   23.26  by (auto, drule Standard_minus, auto)
   23.27 @@ -68,7 +68,7 @@
   23.28  done
   23.29  
   23.30  
   23.31 -subsection{*The Finite Elements form a Subring*}
   23.32 +subsection\<open>The Finite Elements form a Subring\<close>
   23.33  
   23.34  lemma HFinite_hcmod_hcomplex_of_complex [simp]:
   23.35       "hcmod (hcomplex_of_complex r) \<in> HFinite"
   23.36 @@ -82,7 +82,7 @@
   23.37  by (auto intro: HFinite_bounded simp add: HFinite_hcmod_iff)
   23.38  
   23.39  
   23.40 -subsection{*The Complex Infinitesimals form a Subring*}
   23.41 +subsection\<open>The Complex Infinitesimals form a Subring\<close>
   23.42  
   23.43  lemma hcomplex_sum_of_halves: "x/(2::hcomplex) + x/(2::hcomplex) = x"
   23.44  by auto
   23.45 @@ -121,7 +121,7 @@
   23.46  by (auto intro: Infinitesimal_interval2 simp add: Infinitesimal_hcmod_iff)
   23.47  
   23.48  
   23.49 -subsection{*The ``Infinitely Close'' Relation*}
   23.50 +subsection\<open>The ``Infinitely Close'' Relation\<close>
   23.51  
   23.52  (*
   23.53  Goalw [capprox_def,approx_def] "(z @c= w) = (hcmod z @= hcmod w)"
   23.54 @@ -183,7 +183,7 @@
   23.55  done
   23.56  
   23.57  
   23.58 -subsection{*Zero is the Only Infinitesimal Complex Number*}
   23.59 +subsection\<open>Zero is the Only Infinitesimal Complex Number\<close>
   23.60  
   23.61  lemma Infinitesimal_less_SComplex:
   23.62     "[| x \<in> SComplex; y \<in> Infinitesimal; 0 < hcmod x |] ==> hcmod y < hcmod x"
   23.63 @@ -229,7 +229,7 @@
   23.64       "[| r \<in> SComplex; s \<in> SComplex; r @= x; s @= x|] ==> r = s"
   23.65  by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2)
   23.66  
   23.67 -subsection {* Properties of @{term hRe}, @{term hIm} and @{term HComplex} *}
   23.68 +subsection \<open>Properties of @{term hRe}, @{term hIm} and @{term HComplex}\<close>
   23.69  
   23.70  
   23.71  lemma abs_hRe_le_hcmod: "\<And>x. \<bar>hRe x\<bar> \<le> hcmod x"
   23.72 @@ -360,13 +360,13 @@
   23.73    hcomplex_of_complex_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
   23.74  
   23.75  
   23.76 -subsection{*Theorems About Monads*}
   23.77 +subsection\<open>Theorems About Monads\<close>
   23.78  
   23.79  lemma monad_zero_hcmod_iff: "(x \<in> monad 0) = (hcmod x:monad 0)"
   23.80  by (simp add: Infinitesimal_monad_zero_iff [symmetric] Infinitesimal_hcmod_iff)
   23.81  
   23.82  
   23.83 -subsection{*Theorems About Standard Part*}
   23.84 +subsection\<open>Theorems About Standard Part\<close>
   23.85  
   23.86  lemma stc_approx_self: "x \<in> HFinite ==> stc x @= x"
   23.87  apply (simp add: stc_def)
    24.1 --- a/src/HOL/NSA/NSComplex.thy	Wed Dec 30 11:32:56 2015 +0100
    24.2 +++ b/src/HOL/NSA/NSComplex.thy	Wed Dec 30 11:37:29 2015 +0100
    24.3 @@ -3,7 +3,7 @@
    24.4      Author:     Lawrence C Paulson
    24.5  *)
    24.6  
    24.7 -section{*Nonstandard Complex Numbers*}
    24.8 +section\<open>Nonstandard Complex Numbers\<close>
    24.9  
   24.10  theory NSComplex
   24.11  imports NSA
   24.12 @@ -118,7 +118,7 @@
   24.13  by (rule hnorm_def)
   24.14  
   24.15  
   24.16 -subsection{*Properties of Nonstandard Real and Imaginary Parts*}
   24.17 +subsection\<open>Properties of Nonstandard Real and Imaginary Parts\<close>
   24.18  
   24.19  lemma hcomplex_hRe_hIm_cancel_iff:
   24.20       "!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
   24.21 @@ -141,7 +141,7 @@
   24.22  by transfer simp
   24.23  
   24.24  
   24.25 -subsection{*Addition for Nonstandard Complex Numbers*}
   24.26 +subsection\<open>Addition for Nonstandard Complex Numbers\<close>
   24.27  
   24.28  lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)"
   24.29  by transfer simp
   24.30 @@ -149,7 +149,7 @@
   24.31  lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
   24.32  by transfer simp
   24.33  
   24.34 -subsection{*More Minus Laws*}
   24.35 +subsection\<open>More Minus Laws\<close>
   24.36  
   24.37  lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
   24.38  by transfer (rule uminus_complex.sel)
   24.39 @@ -173,7 +173,7 @@
   24.40  by transfer (rule complex_i_not_zero)
   24.41  
   24.42  
   24.43 -subsection{*More Multiplication Laws*}
   24.44 +subsection\<open>More Multiplication Laws\<close>
   24.45  
   24.46  lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z"
   24.47  by simp
   24.48 @@ -190,14 +190,14 @@
   24.49  by simp
   24.50  
   24.51  
   24.52 -subsection{*Subraction and Division*}
   24.53 +subsection\<open>Subraction and Division\<close>
   24.54  
   24.55  lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)"
   24.56  (* TODO: delete *)
   24.57  by (rule diff_eq_eq)
   24.58  
   24.59  
   24.60 -subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
   24.61 +subsection\<open>Embedding Properties for @{term hcomplex_of_hypreal} Map\<close>
   24.62  
   24.63  lemma hRe_hcomplex_of_hypreal [simp]: "!!z. hRe(hcomplex_of_hypreal z) = z"
   24.64  by transfer (rule Re_complex_of_real)
   24.65 @@ -209,7 +209,7 @@
   24.66       "hcomplex_of_hypreal epsilon \<noteq> 0"
   24.67  by (simp add: hypreal_epsilon_not_zero)
   24.68  
   24.69 -subsection{*HComplex theorems*}
   24.70 +subsection\<open>HComplex theorems\<close>
   24.71  
   24.72  lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x"
   24.73  by transfer simp
   24.74 @@ -225,7 +225,7 @@
   24.75  by (rule hcomplex_surj [THEN subst], blast)
   24.76  
   24.77  
   24.78 -subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
   24.79 +subsection\<open>Modulus (Absolute Value) of Nonstandard Complex Number\<close>
   24.80  
   24.81  lemma hcomplex_of_hypreal_abs:
   24.82       "hcomplex_of_hypreal \<bar>x\<bar> =
   24.83 @@ -282,7 +282,7 @@
   24.84  by transfer (rule complex_of_real_i)
   24.85  
   24.86  
   24.87 -subsection{*Conjugation*}
   24.88 +subsection\<open>Conjugation\<close>
   24.89  
   24.90  lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)"
   24.91  by transfer (rule complex_cnj_cancel_iff)
   24.92 @@ -329,7 +329,7 @@
   24.93  by transfer (rule complex_mult_cnj)
   24.94  
   24.95  
   24.96 -subsection{*More Theorems about the Function @{term hcmod}*}
   24.97 +subsection\<open>More Theorems about the Function @{term hcmod}\<close>
   24.98  
   24.99  lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
  24.100       "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
  24.101 @@ -350,7 +350,7 @@
  24.102  by transfer (rule norm_diff_ineq)
  24.103  
  24.104  
  24.105 -subsection{*Exponentiation*}
  24.106 +subsection\<open>Exponentiation\<close>
  24.107  
  24.108  lemma hcomplexpow_0 [simp]:   "z ^ 0       = (1::hcomplex)"
  24.109  by (rule power_0)
  24.110 @@ -392,7 +392,7 @@
  24.111    "r pow n = (0::hcomplex) ==> r = 0"
  24.112    by (blast intro: ccontr dest: hcpow_not_zero)
  24.113  
  24.114 -subsection{*The Function @{term hsgn}*}
  24.115 +subsection\<open>The Function @{term hsgn}\<close>
  24.116  
  24.117  lemma hsgn_zero [simp]: "hsgn 0 = 0"
  24.118  by transfer (rule sgn_zero)
  24.119 @@ -466,7 +466,7 @@
  24.120  by transfer (rule of_real_eq_0_iff)
  24.121  
  24.122  
  24.123 -subsection{*Polar Form for Nonstandard Complex Numbers*}
  24.124 +subsection\<open>Polar Form for Nonstandard Complex Numbers\<close>
  24.125  
  24.126  lemma complex_split_polar2:
  24.127       "\<forall>n. \<exists>r a. (z n) =  complex_of_real r * (Complex (cos a) (sin a))"
  24.128 @@ -599,8 +599,8 @@
  24.129  by transfer (rule exp_add)
  24.130  
  24.131  
  24.132 -subsection{*@{term hcomplex_of_complex}: the Injection from
  24.133 -  type @{typ complex} to to @{typ hcomplex}*}
  24.134 +subsection\<open>@{term hcomplex_of_complex}: the Injection from
  24.135 +  type @{typ complex} to to @{typ hcomplex}\<close>
  24.136  
  24.137  lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
  24.138  by (rule iii_def)
  24.139 @@ -618,7 +618,7 @@
  24.140  by transfer (rule refl)
  24.141  
  24.142  
  24.143 -subsection{*Numerals and Arithmetic*}
  24.144 +subsection\<open>Numerals and Arithmetic\<close>
  24.145  
  24.146  lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
  24.147       "hcomplex_of_hypreal (hypreal_of_real x) =
    25.1 --- a/src/HOL/NSA/NatStar.thy	Wed Dec 30 11:32:56 2015 +0100
    25.2 +++ b/src/HOL/NSA/NatStar.thy	Wed Dec 30 11:37:29 2015 +0100
    25.3 @@ -5,7 +5,7 @@
    25.4  Converted to Isar and polished by lcp
    25.5  *)
    25.6  
    25.7 -section{*Star-transforms for the Hypernaturals*}
    25.8 +section\<open>Star-transforms for the Hypernaturals\<close>
    25.9  
   25.10  theory NatStar
   25.11  imports Star
   25.12 @@ -72,10 +72,10 @@
   25.13  by (auto intro: InternalSets_Compl)
   25.14  
   25.15  
   25.16 -subsection{*Nonstandard Extensions of Functions*}
   25.17 +subsection\<open>Nonstandard Extensions of Functions\<close>
   25.18  
   25.19 -text{* Example of transfer of a property from reals to hyperreals
   25.20 -    --- used for limit comparison of sequences*}
   25.21 +text\<open>Example of transfer of a property from reals to hyperreals
   25.22 +    --- used for limit comparison of sequences\<close>
   25.23  
   25.24  lemma starfun_le_mono:
   25.25       "\<forall>n. N \<le> n --> f n \<le> g n
   25.26 @@ -88,18 +88,18 @@
   25.27        ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *f* f) n < ( *f* g) n"
   25.28  by transfer
   25.29  
   25.30 -text{*Nonstandard extension when we increment the argument by one*}
   25.31 +text\<open>Nonstandard extension when we increment the argument by one\<close>
   25.32  
   25.33  lemma starfun_shift_one:
   25.34       "!!N. ( *f* (%n. f (Suc n))) N = ( *f* f) (N + (1::hypnat))"
   25.35  by (transfer, simp)
   25.36  
   25.37 -text{*Nonstandard extension with absolute value*}
   25.38 +text\<open>Nonstandard extension with absolute value\<close>
   25.39  
   25.40  lemma starfun_abs: "!!N. ( *f* (%n. \<bar>f n\<bar>)) N = \<bar>( *f* f) N\<bar>"
   25.41  by (transfer, rule refl)
   25.42  
   25.43 -text{*The hyperpow function as a nonstandard extension of realpow*}
   25.44 +text\<open>The hyperpow function as a nonstandard extension of realpow\<close>
   25.45  
   25.46  lemma starfun_pow: "!!N. ( *f* (%n. r ^ n)) N = (hypreal_of_real r) pow N"
   25.47  by (transfer, rule refl)
   25.48 @@ -111,8 +111,8 @@
   25.49  lemma starfun_pow3: "!!R. ( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"
   25.50  by (transfer, rule refl)
   25.51  
   25.52 -text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of
   25.53 -  @{term real_of_nat} *}
   25.54 +text\<open>The @{term hypreal_of_hypnat} function as a nonstandard extension of
   25.55 +  @{term real_of_nat}\<close>
   25.56  
   25.57  lemma starfunNat_real_of_nat: "( *f* real) = hypreal_of_hypnat"
   25.58  by transfer (simp add: fun_eq_iff)
   25.59 @@ -125,12 +125,12 @@
   25.60  apply (simp_all add: zero_less_HNatInfinite starfunNat_real_of_nat starfun_inverse_inverse)
   25.61  done
   25.62  
   25.63 -text{*Internal functions - some redundancy with *f* now*}
   25.64 +text\<open>Internal functions - some redundancy with *f* now\<close>
   25.65  
   25.66  lemma starfun_n: "( *fn* f) (star_n X) = star_n (%n. f n (X n))"
   25.67  by (simp add: starfun_n_def Ifun_star_n)
   25.68  
   25.69 -text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*}
   25.70 +text\<open>Multiplication: \<open>( *fn) x ( *gn) = *(fn x gn)\<close>\<close>
   25.71  
   25.72  lemma starfun_n_mult:
   25.73       "( *fn* f) z * ( *fn* g) z = ( *fn* (% i x. f i x * g i x)) z"
   25.74 @@ -138,7 +138,7 @@
   25.75  apply (simp add: starfun_n star_n_mult)
   25.76  done
   25.77  
   25.78 -text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*}
   25.79 +text\<open>Addition: \<open>( *fn) + ( *gn) = *(fn + gn)\<close>\<close>
   25.80  
   25.81  lemma starfun_n_add:
   25.82       "( *fn* f) z + ( *fn* g) z = ( *fn* (%i x. f i x + g i x)) z"
   25.83 @@ -146,7 +146,7 @@
   25.84  apply (simp add: starfun_n star_n_add)
   25.85  done
   25.86  
   25.87 -text{*Subtraction: @{text "( *fn) - ( *gn) = *(fn + - gn)"}*}
   25.88 +text\<open>Subtraction: \<open>( *fn) - ( *gn) = *(fn + - gn)\<close>\<close>
   25.89  
   25.90  lemma starfun_n_add_minus:
   25.91       "( *fn* f) z + -( *fn* g) z = ( *fn* (%i x. f i x + -g i x)) z"
   25.92 @@ -155,7 +155,7 @@
   25.93  done
   25.94  
   25.95  
   25.96 -text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*}
   25.97 +text\<open>Composition: \<open>( *fn) o ( *gn) = *(fn o gn)\<close>\<close>
   25.98  
   25.99  lemma starfun_n_const_fun [simp]:
  25.100       "( *fn* (%i x. k)) z = star_of k"
  25.101 @@ -183,7 +183,7 @@
  25.102  done
  25.103  
  25.104  
  25.105 -subsection{*Nonstandard Characterization of Induction*}
  25.106 +subsection\<open>Nonstandard Characterization of Induction\<close>
  25.107  
  25.108  lemma hypnat_induct_obj:
  25.109      "!!n. (( *p* P) (0::hypnat) &
  25.110 @@ -221,7 +221,7 @@
  25.111  apply (erule nonempty_set_star_has_least)
  25.112  done
  25.113  
  25.114 -text{* Goldblatt page 129 Thm 11.3.2*}
  25.115 +text\<open>Goldblatt page 129 Thm 11.3.2\<close>
  25.116  lemma internal_induct_lemma:
  25.117       "!!X::nat set star. [| (0::hypnat) \<in> Iset X; \<forall>n. n \<in> Iset X --> n + 1 \<in> Iset X |]
  25.118        ==> Iset X = (UNIV:: hypnat set)"
    26.1 --- a/src/HOL/NSA/Star.thy	Wed Dec 30 11:32:56 2015 +0100
    26.2 +++ b/src/HOL/NSA/Star.thy	Wed Dec 30 11:37:29 2015 +0100
    26.3 @@ -4,7 +4,7 @@
    26.4      Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
    26.5  *)
    26.6  
    26.7 -section{*Star-Transforms in Non-Standard Analysis*}
    26.8 +section\<open>Star-Transforms in Non-Standard Analysis\<close>
    26.9  
   26.10  theory Star
   26.11  imports NSA
   26.12 @@ -48,7 +48,7 @@
   26.13  apply (blast intro: LeastI)
   26.14  done
   26.15  
   26.16 -subsection{*Properties of the Star-transform Applied to Sets of Reals*}
   26.17 +subsection\<open>Properties of the Star-transform Applied to Sets of Reals\<close>
   26.18  
   26.19  lemma STAR_star_of_image_subset: "star_of ` A <= *s* A"
   26.20  by auto
   26.21 @@ -83,8 +83,8 @@
   26.22  lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
   26.23  by (erule rev_subsetD, simp)
   26.24  
   26.25 -text{*Nonstandard extension of a set (defined using a constant
   26.26 -   sequence) as a special case of an internal set*}
   26.27 +text\<open>Nonstandard extension of a set (defined using a constant
   26.28 +   sequence) as a special case of an internal set\<close>
   26.29  
   26.30  lemma starset_n_starset: "\<forall>n. (As n = A) ==> *sn* As = *s* A"
   26.31  apply (drule fun_eq_iff [THEN iffD2])
   26.32 @@ -127,7 +127,7 @@
   26.33  apply (simp add: Ifun_star_n star_n_eq_iff)
   26.34  done
   26.35  
   26.36 -text{*Nonstandard extension of functions*}
   26.37 +text\<open>Nonstandard extension of functions\<close>
   26.38  
   26.39  lemma starfun:
   26.40        "( *f* f) (star_n X) = star_n (%n. f (X n))"
   26.41 @@ -178,11 +178,11 @@
   26.42  lemma starfun_o: "( *f* f) o ( *f* g) = ( *f* (f o g))"
   26.43  by (transfer o_def, rule refl)
   26.44  
   26.45 -text{*NS extension of constant function*}
   26.46 +text\<open>NS extension of constant function\<close>
   26.47  lemma starfun_const_fun [simp]: "!!x. ( *f* (%x. k)) x = star_of k"
   26.48  by (transfer, rule refl)
   26.49  
   26.50 -text{*the NS extension of the identity function*}
   26.51 +text\<open>the NS extension of the identity function\<close>
   26.52  
   26.53  lemma starfun_Id [simp]: "!!x. ( *f* (%x. x)) x = x"
   26.54  by (transfer, rule refl)
   26.55 @@ -192,7 +192,7 @@
   26.56    "x @= star_of a ==> ( *f* (%x. x)) x @= star_of a"
   26.57  by (simp only: starfun_Id)
   26.58  
   26.59 -text{*The Star-function is a (nonstandard) extension of the function*}
   26.60 +text\<open>The Star-function is a (nonstandard) extension of the function\<close>
   26.61  
   26.62  lemma is_starext_starfun: "is_starext ( *f* f) f"
   26.63  apply (simp add: is_starext_def, auto)
   26.64 @@ -202,7 +202,7 @@
   26.65              simp add: starfun star_n_eq_iff)
   26.66  done
   26.67  
   26.68 -text{*Any nonstandard extension is in fact the Star-function*}
   26.69 +text\<open>Any nonstandard extension is in fact the Star-function\<close>
   26.70  
   26.71  lemma is_starfun_starext: "is_starext F f ==> F = *f* f"
   26.72  apply (simp add: is_starext_def)
   26.73 @@ -218,9 +218,9 @@
   26.74  lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)"
   26.75  by (blast intro: is_starfun_starext is_starext_starfun)
   26.76  
   26.77 -text{*extented function has same solution as its standard
   26.78 +text\<open>extented function has same solution as its standard
   26.79     version for real arguments. i.e they are the same
   26.80 -   for all real arguments*}
   26.81 +   for all real arguments\<close>
   26.82  lemma starfun_eq: "( *f* f) (star_of a) = star_of (f a)"
   26.83  by (rule starfun_star_of)
   26.84  
   26.85 @@ -249,8 +249,8 @@
   26.86                 |] ==>  ( *f* (%x. f x + g x)) x @= l + m"
   26.87  by (auto intro: approx_add)
   26.88  
   26.89 -text{*Examples: hrabs is nonstandard extension of rabs
   26.90 -              inverse is nonstandard extension of inverse*}
   26.91 +text\<open>Examples: hrabs is nonstandard extension of rabs
   26.92 +              inverse is nonstandard extension of inverse\<close>
   26.93  
   26.94  (* can be proved easily using theorem "starfun" and *)
   26.95  (* properties of ultrafilter as for inverse below we  *)
   26.96 @@ -273,22 +273,22 @@
   26.97  lemma starfun_inverse2: "!!x. inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
   26.98  by (transfer, rule refl)
   26.99  
  26.100 -text{*General lemma/theorem needed for proofs in elementary
  26.101 -    topology of the reals*}
  26.102 +text\<open>General lemma/theorem needed for proofs in elementary
  26.103 +    topology of the reals\<close>
  26.104  lemma starfun_mem_starset:
  26.105        "!!x. ( *f* f) x : *s* A ==> x : *s* {x. f x  \<in> A}"
  26.106  by (transfer, simp)
  26.107  
  26.108 -text{*Alternative definition for hrabs with rabs function
  26.109 +text\<open>Alternative definition for hrabs with rabs function
  26.110     applied entrywise to equivalence class representative.
  26.111 -   This is easily proved using starfun and ns extension thm*}
  26.112 +   This is easily proved using starfun and ns extension thm\<close>
  26.113  lemma hypreal_hrabs: "\<bar>star_n X\<bar> = star_n (%n. \<bar>X n\<bar>)"
  26.114  by (simp only: starfun_rabs_hrabs [symmetric] starfun)
  26.115  
  26.116 -text{*nonstandard extension of set through nonstandard extension
  26.117 +text\<open>nonstandard extension of set through nonstandard extension
  26.118     of rabs function i.e hrabs. A more general result should be
  26.119     where we replace rabs by some arbitrary function f and hrabs
  26.120 -   by its NS extenson. See second NS set extension below.*}
  26.121 +   by its NS extenson. See second NS set extension below.\<close>
  26.122  lemma STAR_rabs_add_minus:
  26.123     "*s* {x. \<bar>x + - y\<bar> < r} = {x. \<bar>x + -star_of y\<bar> < star_of r}"
  26.124  by (transfer, rule refl)
  26.125 @@ -298,9 +298,9 @@
  26.126         {x. \<bar>( *f* f) x + -star_of y\<bar> < star_of r}"
  26.127  by (transfer, rule refl)
  26.128  
  26.129 -text{*Another characterization of Infinitesimal and one of @= relation.
  26.130 -   In this theory since @{text hypreal_hrabs} proved here. Maybe
  26.131 -   move both theorems??*}
  26.132 +text\<open>Another characterization of Infinitesimal and one of @= relation.
  26.133 +   In this theory since \<open>hypreal_hrabs\<close> proved here. Maybe
  26.134 +   move both theorems??\<close>
  26.135  lemma Infinitesimal_FreeUltrafilterNat_iff2:
  26.136       "(star_n X \<in> Infinitesimal) = (\<forall>m. eventually (\<lambda>n. norm(X n) < inverse(real(Suc m))) \<U>)"
  26.137  by (simp add: Infinitesimal_hypreal_of_nat_iff star_of_def
    27.1 --- a/src/HOL/NSA/StarDef.thy	Wed Dec 30 11:32:56 2015 +0100
    27.2 +++ b/src/HOL/NSA/StarDef.thy	Wed Dec 30 11:37:29 2015 +0100
    27.3 @@ -2,13 +2,13 @@
    27.4      Author      : Jacques D. Fleuriot and Brian Huffman
    27.5  *)
    27.6  
    27.7 -section {* Construction of Star Types Using Ultrafilters *}
    27.8 +section \<open>Construction of Star Types Using Ultrafilters\<close>
    27.9  
   27.10  theory StarDef
   27.11  imports Free_Ultrafilter
   27.12  begin
   27.13  
   27.14 -subsection {* A Free Ultrafilter over the Naturals *}
   27.15 +subsection \<open>A Free Ultrafilter over the Naturals\<close>
   27.16  
   27.17  definition
   27.18    FreeUltrafilterNat :: "nat filter"  ("\<U>") where
   27.19 @@ -24,7 +24,7 @@
   27.20  interpretation FreeUltrafilterNat: freeultrafilter FreeUltrafilterNat
   27.21  by (rule freeultrafilter_FreeUltrafilterNat)
   27.22  
   27.23 -subsection {* Definition of @{text star} type constructor *}
   27.24 +subsection \<open>Definition of \<open>star\<close> type constructor\<close>
   27.25  
   27.26  definition
   27.27    starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where
   27.28 @@ -49,7 +49,7 @@
   27.29  lemma ex_star_eq: "(\<exists>x. P x) = (\<exists>X. P (star_n X))"
   27.30  by (auto, rule_tac x=x in star_cases, auto)
   27.31  
   27.32 -text {* Proving that @{term starrel} is an equivalence relation *}
   27.33 +text \<open>Proving that @{term starrel} is an equivalence relation\<close>
   27.34  
   27.35  lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = (eventually (\<lambda>n. X n = Y n) \<U>)"
   27.36  by (simp add: starrel_def)
   27.37 @@ -71,23 +71,23 @@
   27.38  by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff)
   27.39  
   27.40  
   27.41 -subsection {* Transfer principle *}
   27.42 +subsection \<open>Transfer principle\<close>
   27.43  
   27.44 -text {* This introduction rule starts each transfer proof. *}
   27.45 +text \<open>This introduction rule starts each transfer proof.\<close>
   27.46  lemma transfer_start:
   27.47    "P \<equiv> eventually (\<lambda>n. Q) \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q"
   27.48    by (simp add: FreeUltrafilterNat.proper)
   27.49  
   27.50 -text {*Initialize transfer tactic.*}
   27.51 +text \<open>Initialize transfer tactic.\<close>
   27.52  ML_file "transfer.ML"
   27.53  
   27.54 -method_setup transfer = {*
   27.55 +method_setup transfer = \<open>
   27.56    Attrib.thms >> (fn ths => fn ctxt =>
   27.57      SIMPLE_METHOD' (Transfer_Principle.transfer_tac ctxt ths))
   27.58 -*} "transfer principle"
   27.59 +\<close> "transfer principle"
   27.60  
   27.61  
   27.62 -text {* Transfer introduction rules. *}
   27.63 +text \<open>Transfer introduction rules.\<close>
   27.64  
   27.65  lemma transfer_ex [transfer_intro]:
   27.66    "\<lbrakk>\<And>X. p (star_n X) \<equiv> eventually (\<lambda>n. P n (X n)) \<U>\<rbrakk>
   27.67 @@ -152,7 +152,7 @@
   27.68  by (simp add: FreeUltrafilterNat.proper)
   27.69  
   27.70  
   27.71 -subsection {* Standard elements *}
   27.72 +subsection \<open>Standard elements\<close>
   27.73  
   27.74  definition
   27.75    star_of :: "'a \<Rightarrow> 'a star" where
   27.76 @@ -162,8 +162,8 @@
   27.77    Standard :: "'a star set" where
   27.78    "Standard = range star_of"
   27.79  
   27.80 -text {* Transfer tactic should remove occurrences of @{term star_of} *}
   27.81 -setup {* Transfer_Principle.add_const @{const_name star_of} *}
   27.82 +text \<open>Transfer tactic should remove occurrences of @{term star_of}\<close>
   27.83 +setup \<open>Transfer_Principle.add_const @{const_name star_of}\<close>
   27.84  
   27.85  declare star_of_def [transfer_intro]
   27.86  
   27.87 @@ -174,7 +174,7 @@
   27.88  by (simp add: Standard_def)
   27.89  
   27.90  
   27.91 -subsection {* Internal functions *}
   27.92 +subsection \<open>Internal functions\<close>
   27.93  
   27.94  definition
   27.95    Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300) where
   27.96 @@ -189,8 +189,8 @@
   27.97  by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star
   27.98      UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
   27.99  
  27.100 -text {* Transfer tactic should remove occurrences of @{term Ifun} *}
  27.101 -setup {* Transfer_Principle.add_const @{const_name Ifun} *}
  27.102 +text \<open>Transfer tactic should remove occurrences of @{term Ifun}\<close>
  27.103 +setup \<open>Transfer_Principle.add_const @{const_name Ifun}\<close>
  27.104  
  27.105  lemma transfer_Ifun [transfer_intro]:
  27.106    "\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
  27.107 @@ -203,7 +203,7 @@
  27.108    "\<lbrakk>f \<in> Standard; x \<in> Standard\<rbrakk> \<Longrightarrow> f \<star> x \<in> Standard"
  27.109  by (auto simp add: Standard_def)
  27.110  
  27.111 -text {* Nonstandard extensions of functions *}
  27.112 +text \<open>Nonstandard extensions of functions\<close>
  27.113  
  27.114  definition
  27.115    starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)"  ("*f* _" [80] 80) where
  27.116 @@ -285,7 +285,7 @@
  27.117  qed
  27.118  
  27.119  
  27.120 -subsection {* Internal predicates *}
  27.121 +subsection \<open>Internal predicates\<close>
  27.122  
  27.123  definition unstar :: "bool star \<Rightarrow> bool" where
  27.124    "unstar b \<longleftrightarrow> b = star_of True"
  27.125 @@ -296,8 +296,8 @@
  27.126  lemma unstar_star_of [simp]: "unstar (star_of p) = p"
  27.127  by (simp add: unstar_def star_of_inject)
  27.128  
  27.129 -text {* Transfer tactic should remove occurrences of @{term unstar} *}
  27.130 -setup {* Transfer_Principle.add_const @{const_name unstar} *}
  27.131 +text \<open>Transfer tactic should remove occurrences of @{term unstar}\<close>
  27.132 +setup \<open>Transfer_Principle.add_const @{const_name unstar}\<close>
  27.133  
  27.134  lemma transfer_unstar [transfer_intro]:
  27.135    "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> eventually P \<U>"
  27.136 @@ -328,7 +328,7 @@
  27.137  by (transfer, rule refl)
  27.138  
  27.139  
  27.140 -subsection {* Internal sets *}
  27.141 +subsection \<open>Internal sets\<close>
  27.142  
  27.143  definition
  27.144    Iset :: "'a set star \<Rightarrow> 'a star set" where
  27.145 @@ -338,8 +338,8 @@
  27.146    "(star_n X \<in> Iset (star_n A)) = (eventually (\<lambda>n. X n \<in> A n) \<U>)"
  27.147  by (simp add: Iset_def starP2_star_n)
  27.148  
  27.149 -text {* Transfer tactic should remove occurrences of @{term Iset} *}
  27.150 -setup {* Transfer_Principle.add_const @{const_name Iset} *}
  27.151 +text \<open>Transfer tactic should remove occurrences of @{term Iset}\<close>
  27.152 +setup \<open>Transfer_Principle.add_const @{const_name Iset}\<close>
  27.153  
  27.154  lemma transfer_mem [transfer_intro]:
  27.155    "\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
  27.156 @@ -370,7 +370,7 @@
  27.157    "\<lbrakk>a \<equiv> star_n A\<rbrakk> \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))"
  27.158  by simp
  27.159  
  27.160 -text {* Nonstandard extensions of sets. *}
  27.161 +text \<open>Nonstandard extensions of sets.\<close>
  27.162  
  27.163  definition
  27.164    starset :: "'a set \<Rightarrow> 'a star set" ("*s* _" [80] 80) where
  27.165 @@ -423,7 +423,7 @@
  27.166    starset_subset  starset_eq
  27.167  
  27.168  
  27.169 -subsection {* Syntactic classes *}
  27.170 +subsection \<open>Syntactic classes\<close>
  27.171  
  27.172  instantiation star :: (zero) zero
  27.173  begin
  27.174 @@ -557,7 +557,7 @@
  27.175    star_le_def       star_less_def     star_abs_def       star_sgn_def
  27.176    star_mod_def
  27.177  
  27.178 -text {* Class operations preserve standard elements *}
  27.179 +text \<open>Class operations preserve standard elements\<close>
  27.180  
  27.181  lemma Standard_zero: "0 \<in> Standard"
  27.182  by (simp add: star_zero_def)
  27.183 @@ -595,7 +595,7 @@
  27.184    Standard_mult  Standard_divide  Standard_inverse
  27.185    Standard_abs   Standard_mod
  27.186  
  27.187 -text {* @{term star_of} preserves class operations *}
  27.188 +text \<open>@{term star_of} preserves class operations\<close>
  27.189  
  27.190  lemma star_of_add: "star_of (x + y) = star_of x + star_of y"
  27.191  by transfer (rule refl)
  27.192 @@ -621,7 +621,7 @@
  27.193  lemma star_of_abs: "star_of \<bar>x\<bar> = \<bar>star_of x\<bar>"
  27.194  by transfer (rule refl)
  27.195  
  27.196 -text {* @{term star_of} preserves numerals *}
  27.197 +text \<open>@{term star_of} preserves numerals\<close>
  27.198  
  27.199  lemma star_of_zero: "star_of 0 = 0"
  27.200  by transfer (rule refl)
  27.201 @@ -629,7 +629,7 @@
  27.202  lemma star_of_one: "star_of 1 = 1"
  27.203  by transfer (rule refl)
  27.204  
  27.205 -text {* @{term star_of} preserves orderings *}
  27.206 +text \<open>@{term star_of} preserves orderings\<close>
  27.207  
  27.208  lemma star_of_less: "(star_of x < star_of y) = (x < y)"
  27.209  by transfer (rule refl)
  27.210 @@ -640,7 +640,7 @@
  27.211  lemma star_of_eq: "(star_of x = star_of y) = (x = y)"
  27.212  by transfer (rule refl)
  27.213  
  27.214 -text{*As above, for 0*}
  27.215 +text\<open>As above, for 0\<close>
  27.216  
  27.217  lemmas star_of_0_less = star_of_less [of 0, simplified star_of_zero]
  27.218  lemmas star_of_0_le   = star_of_le   [of 0, simplified star_of_zero]
  27.219 @@ -650,7 +650,7 @@
  27.220  lemmas star_of_le_0   = star_of_le   [of _ 0, simplified star_of_zero]
  27.221  lemmas star_of_eq_0   = star_of_eq   [of _ 0, simplified star_of_zero]
  27.222  
  27.223 -text{*As above, for 1*}
  27.224 +text\<open>As above, for 1\<close>
  27.225  
  27.226  lemmas star_of_1_less = star_of_less [of 1, simplified star_of_one]
  27.227  lemmas star_of_1_le   = star_of_le   [of 1, simplified star_of_one]
  27.228 @@ -671,7 +671,7 @@
  27.229    star_of_1_less  star_of_1_le    star_of_1_eq
  27.230    star_of_less_1  star_of_le_1    star_of_eq_1
  27.231  
  27.232 -subsection {* Ordering and lattice classes *}
  27.233 +subsection \<open>Ordering and lattice classes\<close>
  27.234  
  27.235  instance star :: (order) order
  27.236  apply (intro_classes)
  27.237 @@ -752,7 +752,7 @@
  27.238  by transfer (rule refl)
  27.239  
  27.240  
  27.241 -subsection {* Ordered group classes *}
  27.242 +subsection \<open>Ordered group classes\<close>
  27.243  
  27.244  instance star :: (semigroup_add) semigroup_add
  27.245  by (intro_classes, transfer, rule add.assoc)
  27.246 @@ -815,7 +815,7 @@
  27.247  instance star :: (linordered_cancel_ab_semigroup_add) linordered_cancel_ab_semigroup_add ..
  27.248  
  27.249  
  27.250 -subsection {* Ring and field classes *}
  27.251 +subsection \<open>Ring and field classes\<close>
  27.252  
  27.253  instance star :: (semiring) semiring
  27.254    by (intro_classes; transfer) (fact distrib_right distrib_left)+
  27.255 @@ -913,7 +913,7 @@
  27.256  instance star :: (linordered_idom) linordered_idom ..
  27.257  instance star :: (linordered_field) linordered_field ..
  27.258  
  27.259 -subsection {* Power *}
  27.260 +subsection \<open>Power\<close>
  27.261  
  27.262  lemma star_power_def [transfer_unfold]:
  27.263    "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
  27.264 @@ -940,7 +940,7 @@
  27.265    by transfer (rule refl)
  27.266  
  27.267  
  27.268 -subsection {* Number classes *}
  27.269 +subsection \<open>Number classes\<close>
  27.270  
  27.271  instance star :: (numeral) numeral ..
  27.272  
  27.273 @@ -1046,7 +1046,7 @@
  27.274  declare divmod_algorithm_code [where ?'a = "'a::semiring_numeral_div star", code]
  27.275  
  27.276  
  27.277 -subsection {* Finite class *}
  27.278 +subsection \<open>Finite class\<close>
  27.279  
  27.280  lemma starset_finite: "finite A \<Longrightarrow> *s* A = star_of ` A"
  27.281  by (erule finite_induct, simp_all)