isabelle update_cartouches -c -t;
authorwenzelm
Tue Dec 19 13:58:12 2017 +0100 (17 months ago)
changeset 67226ec32cdaab97b
parent 67225 cb34f5f49a08
child 67227 6f6b26557ea9
child 67228 7c7b76695c90
isabelle update_cartouches -c -t;
src/HOL/Algebra/Complete_Lattice.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Multiplicative_Group.thy
src/HOL/Analysis/Bounded_Linear_Function.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.thy
src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
src/HOL/Divides.thy
src/HOL/Fun.thy
src/HOL/Power.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Probability/Conditional_Expectation.thy
src/HOL/Probability/Essential_Supremum.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Stopping_Time.thy
src/HOL/Real.thy
src/HOL/Rings.thy
src/HOL/SMT_Examples/SMT_Examples.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/Topological_Spaces.thy
src/HOL/ex/Perm_Fragments.thy
     1.1 --- a/src/HOL/Algebra/Complete_Lattice.thy	Tue Dec 19 14:51:27 2017 +0100
     1.2 +++ b/src/HOL/Algebra/Complete_Lattice.thy	Tue Dec 19 13:58:12 2017 +0100
     1.3 @@ -543,7 +543,7 @@
     1.4  end
     1.5  
     1.6  
     1.7 -subsection \<open>Complete lattices where @{text eq} is the Equality\<close>
     1.8 +subsection \<open>Complete lattices where \<open>eq\<close> is the Equality\<close>
     1.9  
    1.10  locale complete_lattice = partial_order +
    1.11    assumes sup_exists:
     2.1 --- a/src/HOL/Algebra/Lattice.thy	Tue Dec 19 14:51:27 2017 +0100
     2.2 +++ b/src/HOL/Algebra/Lattice.thy	Tue Dec 19 13:58:12 2017 +0100
     2.3 @@ -52,11 +52,11 @@
     2.4  
     2.5  definition
     2.6    LEAST_FP :: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("LFP\<index>") where
     2.7 -  "LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    --\<open>least fixed point\<close>
     2.8 +  "LEAST_FP L f = \<Sqinter>\<^bsub>L\<^esub> {u \<in> carrier L. f u \<sqsubseteq>\<^bsub>L\<^esub> u}"    \<comment>\<open>least fixed point\<close>
     2.9  
    2.10  definition
    2.11    GREATEST_FP:: "('a, 'b) gorder_scheme \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a" ("GFP\<index>") where
    2.12 -  "GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    --\<open>greatest fixed point\<close>
    2.13 +  "GREATEST_FP L f = \<Squnion>\<^bsub>L\<^esub> {u \<in> carrier L. u \<sqsubseteq>\<^bsub>L\<^esub> f u}"    \<comment>\<open>greatest fixed point\<close>
    2.14  
    2.15  
    2.16  subsection \<open>Dual operators\<close>
     3.1 --- a/src/HOL/Algebra/Multiplicative_Group.thy	Tue Dec 19 14:51:27 2017 +0100
     3.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Tue Dec 19 13:58:12 2017 +0100
     3.3 @@ -13,8 +13,8 @@
     3.4    UnivPoly
     3.5  begin
     3.6  
     3.7 -section {* Simplification Rules for Polynomials *}
     3.8 -text_raw {* \label{sec:simp-rules} *}
     3.9 +section \<open>Simplification Rules for Polynomials\<close>
    3.10 +text_raw \<open>\label{sec:simp-rules}\<close>
    3.11  
    3.12  lemma (in ring_hom_cring) hom_sub[simp]:
    3.13    assumes "x \<in> carrier R" "y \<in> carrier R"
    3.14 @@ -114,13 +114,13 @@
    3.15  
    3.16  
    3.17  
    3.18 -section {* Properties of the Euler @{text \<phi>}-function *}
    3.19 -text_raw {* \label{sec:euler-phi} *}
    3.20 +section \<open>Properties of the Euler \<open>\<phi>\<close>-function\<close>
    3.21 +text_raw \<open>\label{sec:euler-phi}\<close>
    3.22  
    3.23 -text{*
    3.24 +text\<open>
    3.25    In this section we prove that for every positive natural number the equation
    3.26    $\sum_{d | n}^n \varphi(d) = n$ holds.
    3.27 -*}
    3.28 +\<close>
    3.29  
    3.30  lemma dvd_div_ge_1 :
    3.31    fixes a b :: nat
    3.32 @@ -156,7 +156,7 @@
    3.33  lemma dvd_div_eq_1:
    3.34    fixes a b c :: nat
    3.35    assumes "c dvd a" "c dvd b" "a div c = b div c"
    3.36 -  shows "a = b" using assms dvd_mult_div_cancel[OF `c dvd a`] dvd_mult_div_cancel[OF `c dvd b`]
    3.37 +  shows "a = b" using assms dvd_mult_div_cancel[OF \<open>c dvd a\<close>] dvd_mult_div_cancel[OF \<open>c dvd b\<close>]
    3.38                  by presburger
    3.39  
    3.40  lemma dvd_div_eq_2:
    3.41 @@ -167,7 +167,7 @@
    3.42    have "a > 0" "a \<le> c" using dvd_nat_bounds[OF assms(1-2)] by auto
    3.43    have "a*(c div a) = c" using assms dvd_mult_div_cancel by fastforce
    3.44    also have "\<dots> = b*(c div a)" using assms dvd_mult_div_cancel by fastforce
    3.45 -  finally show "a = b" using `c>0` dvd_div_ge_1[OF _ `a dvd c`] by fastforce
    3.46 +  finally show "a = b" using \<open>c>0\<close> dvd_div_ge_1[OF _ \<open>a dvd c\<close>] by fastforce
    3.47  qed
    3.48  
    3.49  lemma div_mult_mono:
    3.50 @@ -179,7 +179,7 @@
    3.51    thus ?thesis using assms by force
    3.52  qed
    3.53  
    3.54 -text{*
    3.55 +text\<open>
    3.56    We arrive at the main result of this section:
    3.57    For every positive natural number the equation $\sum_{d | n}^n \varphi(d) = n$ holds.
    3.58  
    3.59 @@ -208,7 +208,7 @@
    3.60    and by showing
    3.61    @{term "(\<Union>d \<in> {d. d dvd n}. {m \<in> {1::nat .. n}. n div gcd m n = d}) \<supseteq> {1 .. n}"}
    3.62    (this is our counting argument) the thesis follows.
    3.63 -*}
    3.64 +\<close>
    3.65  lemma sum_phi'_factors :
    3.66   fixes n :: nat
    3.67   assumes "n > 0"
    3.68 @@ -220,19 +220,19 @@
    3.69      proof (rule card_bij_eq)
    3.70        { fix a b assume "a * n div d = b * n div d"
    3.71          hence "a * (n div d) = b * (n div d)"
    3.72 -          using dvd_div_mult[OF `d dvd n`] by (fastforce simp add: mult.commute)
    3.73 -        hence "a = b" using dvd_div_ge_1[OF _ `d dvd n`] `n>0`
    3.74 +          using dvd_div_mult[OF \<open>d dvd n\<close>] by (fastforce simp add: mult.commute)
    3.75 +        hence "a = b" using dvd_div_ge_1[OF _ \<open>d dvd n\<close>] \<open>n>0\<close>
    3.76            by (simp add: mult.commute nat_mult_eq_cancel1)
    3.77        } thus "inj_on (\<lambda>a. a*n div d) ?RF" unfolding inj_on_def by blast
    3.78        { fix a assume a:"a\<in>?RF"
    3.79 -        hence "a * (n div d) \<ge> 1" using `n>0` dvd_div_ge_1[OF _ `d dvd n`] by simp
    3.80 -        hence ge_1:"a * n div d \<ge> 1" by (simp add: `d dvd n` div_mult_swap)
    3.81 +        hence "a * (n div d) \<ge> 1" using \<open>n>0\<close> dvd_div_ge_1[OF _ \<open>d dvd n\<close>] by simp
    3.82 +        hence ge_1:"a * n div d \<ge> 1" by (simp add: \<open>d dvd n\<close> div_mult_swap)
    3.83          have le_n:"a * n div d \<le> n" using div_mult_mono a by simp
    3.84          have "gcd (a * n div d) n = n div d * gcd a d"
    3.85            by (simp add: gcd_mult_distrib_nat q ac_simps)
    3.86          hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
    3.87          hence "a * n div d \<in> ?F"
    3.88 -          using ge_1 le_n by (fastforce simp add: `d dvd n`)
    3.89 +          using ge_1 le_n by (fastforce simp add: \<open>d dvd n\<close>)
    3.90        } thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
    3.91        { fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
    3.92          hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
    3.93 @@ -245,7 +245,7 @@
    3.94      qed force+
    3.95    } hence phi'_eq:"\<And>d. d dvd n \<Longrightarrow> phi' d = card {m \<in> {1 .. n}. n div gcd m n = d}"
    3.96        unfolding phi'_def by presburger
    3.97 -  have fin:"finite {d. d dvd n}" using dvd_nat_bounds[OF `n>0`] by force
    3.98 +  have fin:"finite {d. d dvd n}" using dvd_nat_bounds[OF \<open>n>0\<close>] by force
    3.99    have "(\<Sum>d | d dvd n. phi' d)
   3.100                   = card (\<Union>d \<in> {d. d dvd n}. {m \<in> {1 .. n}. n div gcd m n = d})"
   3.101      using card_UN_disjoint[OF fin, of "(\<lambda>d. {m \<in> {1 .. n}. n div gcd m n = d})"] phi'_eq
   3.102 @@ -262,8 +262,8 @@
   3.103    finally show ?thesis by force
   3.104  qed
   3.105  
   3.106 -section {* Order of an Element of a Group *}
   3.107 -text_raw {* \label{sec:order-elem} *}
   3.108 +section \<open>Order of an Element of a Group\<close>
   3.109 +text_raw \<open>\label{sec:order-elem}\<close>
   3.110  
   3.111  
   3.112  context group begin
   3.113 @@ -365,8 +365,8 @@
   3.114  
   3.115      hence y_x:"y - x \<in> {d \<in> {1.. order G}. a (^) d = \<one>}" using y_x_range by blast
   3.116      have "min (y - x) (ord a) = ord a"
   3.117 -      using Min.in_idem[OF `finite {d \<in> {1 .. order G} . a (^) d = \<one>}` y_x] ord_def by auto
   3.118 -    with `y - x < ord a` have False by linarith
   3.119 +      using Min.in_idem[OF \<open>finite {d \<in> {1 .. order G} . a (^) d = \<one>}\<close> y_x] ord_def by auto
   3.120 +    with \<open>y - x < ord a\<close> have False by linarith
   3.121    }
   3.122    note X = this
   3.123  
   3.124 @@ -392,13 +392,13 @@
   3.125    moreover
   3.126    { assume "x = ord a" "y < ord a"
   3.127      hence "a (^) y = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto
   3.128 -    hence "y=0" using ord_inj[OF assms] `y < ord a` unfolding inj_on_def by force
   3.129 +    hence "y=0" using ord_inj[OF assms] \<open>y < ord a\<close> unfolding inj_on_def by force
   3.130      hence False using A by fastforce
   3.131    }
   3.132    moreover
   3.133    { assume "y = ord a" "x < ord a"
   3.134      hence "a (^) x = a (^) (0::nat)" using pow_ord_eq_1[OF assms] A by auto
   3.135 -    hence "x=0" using ord_inj[OF assms] `x < ord a` unfolding inj_on_def by force
   3.136 +    hence "x=0" using ord_inj[OF assms] \<open>x < ord a\<close> unfolding inj_on_def by force
   3.137      hence False using A by fastforce
   3.138    }
   3.139    ultimately show False using A  by force
   3.140 @@ -418,7 +418,7 @@
   3.141      hence "y = a(^)r" using assms by (simp add: pow_ord_eq_1)
   3.142      have "r < ord a" using ord_ge_1[OF assms] by (simp add: r_def)
   3.143      hence "r \<in> {0 .. ord a - 1}" by (force simp: r_def)
   3.144 -    hence "y \<in> {a(^)x | x. x \<in> {0 .. ord a - 1}}" using `y=a(^)r` by blast
   3.145 +    hence "y \<in> {a(^)x | x. x \<in> {0 .. ord a - 1}}" using \<open>y=a(^)r\<close> by blast
   3.146    }
   3.147    thus "?L \<subseteq> ?R" by auto
   3.148  qed
   3.149 @@ -434,7 +434,7 @@
   3.150    hence "a(^)k = a(^)r" using assms by (simp add: pow_ord_eq_1)
   3.151    hence "a(^)r = \<one>" using assms(3) by simp
   3.152    have "r < ord a" using ord_ge_1[OF assms(1-2)] by (simp add: r_def)
   3.153 -  hence "r = 0" using `a(^)r = \<one>` ord_def[of a] ord_min[of r a] assms(1-2) by linarith
   3.154 +  hence "r = 0" using \<open>a(^)r = \<one>\<close> ord_def[of a] ord_min[of r a] assms(1-2) by linarith
   3.155    thus ?thesis using q by simp
   3.156  qed
   3.157  
   3.158 @@ -463,13 +463,13 @@
   3.159    have ge_1:"ord a div gcd n (ord a) \<ge> 1"
   3.160    proof -
   3.161      have "gcd n (ord a) dvd ord a" by blast
   3.162 -    thus ?thesis by (rule dvd_div_ge_1[OF `ord a \<ge> 1`])
   3.163 +    thus ?thesis by (rule dvd_div_ge_1[OF \<open>ord a \<ge> 1\<close>])
   3.164    qed
   3.165    have "ord a \<le> order G" by (simp add: ord_le_group_order)
   3.166    have "ord a div gcd n (ord a) \<le> order G"
   3.167    proof -
   3.168      have "ord a div gcd n (ord a) \<le> ord a" by simp
   3.169 -    thus ?thesis using `ord a \<le> order G` by linarith
   3.170 +    thus ?thesis using \<open>ord a \<le> order G\<close> by linarith
   3.171    qed
   3.172    hence ord_gcd_elem:"ord a div gcd n (ord a) \<in> {d \<in> {1..order G}. (a(^)n) (^) d = \<one>}"
   3.173      using ge_1 pow_eq_1 by force
   3.174 @@ -537,7 +537,7 @@
   3.175    hence x_in_carrier: "x \<in> carrier G" by auto
   3.176    then obtain d::nat where d:"x (^) d = \<one>" and "d\<ge>1"
   3.177      using finite_group_elem_finite_ord by auto
   3.178 -  have inv_1:"x(^)(d - 1) \<otimes> x = \<one>" using `d\<ge>1` d nat_pow_Suc[of x "d - 1"] by simp
   3.179 +  have inv_1:"x(^)(d - 1) \<otimes> x = \<one>" using \<open>d\<ge>1\<close> d nat_pow_Suc[of x "d - 1"] by simp
   3.180    have elem:"x (^) (d - 1) \<in> {a(^)i | i. i \<in> {0 .. ord a - 1}}"
   3.181    proof -
   3.182      obtain i::nat where i:"x = a(^)i" using x by auto
   3.183 @@ -567,8 +567,8 @@
   3.184  end
   3.185  
   3.186  
   3.187 -section {* Number of Roots of a Polynomial *}
   3.188 -text_raw {* \label{sec:number-roots} *}
   3.189 +section \<open>Number of Roots of a Polynomial\<close>
   3.190 +text_raw \<open>\label{sec:number-roots}\<close>
   3.191  
   3.192  
   3.193  definition mult_of :: "('a, 'b) ring_scheme \<Rightarrow> 'a monoid" where
   3.194 @@ -674,15 +674,15 @@
   3.195                  \<and> card {a \<in> carrier R . eval R R id a q = \<zero>} \<le> x" using Suc q q_not_zero by blast
   3.196      have subs:"{a \<in> carrier R . eval R R id a f = \<zero>}
   3.197                  \<subseteq> {a \<in> carrier R . eval R R id a q = \<zero>} \<union> {a}" (is "?L \<subseteq> ?R \<union> {a}")
   3.198 -      using a_carrier `q \<in> _`
   3.199 +      using a_carrier \<open>q \<in> _\<close>
   3.200        by (auto simp: evalRR_simps lin_fac R.integral_iff)
   3.201      have "{a \<in> carrier R . eval R R id a f = \<zero>} \<subseteq> insert a {a \<in> carrier R . eval R R id a q = \<zero>}"
   3.202       using subs by auto
   3.203      hence "card {a \<in> carrier R . eval R R id a f = \<zero>} \<le>
   3.204             card (insert a {a \<in> carrier R . eval R R id a q = \<zero>})" using q_IH by (blast intro: card_mono)
   3.205 -    also have "\<dots> \<le> deg R f" using q_IH `Suc x = _`
   3.206 +    also have "\<dots> \<le> deg R f" using q_IH \<open>Suc x = _\<close>
   3.207        by (simp add: card_insert_if)
   3.208 -    finally show ?thesis using q_IH `Suc x = _` using finite by force
   3.209 +    finally show ?thesis using q_IH \<open>Suc x = _\<close> using finite by force
   3.210    next
   3.211      case False
   3.212      hence "card {a \<in> carrier R. eval R R id a f = \<zero>} = 0" using finite by auto
   3.213 @@ -712,20 +712,20 @@
   3.214      by (auto simp: R.evalRR_simps)
   3.215    then have "card {x \<in> carrier R. x (^) d = \<one>} \<le>
   3.216          card {a \<in> carrier R. eval R R id a ?f = \<zero>}" using finite by (simp add : card_mono)
   3.217 -  thus ?thesis using `deg R ?f = d` roots_bound by linarith
   3.218 +  thus ?thesis using \<open>deg R ?f = d\<close> roots_bound by linarith
   3.219  qed
   3.220  
   3.221  
   3.222  
   3.223 -section {* The Multiplicative Group of a Field *}
   3.224 -text_raw {* \label{sec:mult-group} *}
   3.225 +section \<open>The Multiplicative Group of a Field\<close>
   3.226 +text_raw \<open>\label{sec:mult-group}\<close>
   3.227  
   3.228  
   3.229 -text {*
   3.230 +text \<open>
   3.231    In this section we show that the multiplicative group of a finite field
   3.232    is generated by a single element, i.e. it is cyclic. The proof is inspired
   3.233    by the first proof given in the survey~\cite{conrad-cyclicity}.
   3.234 -*}
   3.235 +\<close>
   3.236  
   3.237  lemma (in group) pow_order_eq_1:
   3.238    assumes "finite (carrier G)" "x \<in> carrier G" shows "x (^) order G = \<one>"
   3.239 @@ -789,8 +789,8 @@
   3.240          using card_mono[OF finite, of "{\<zero>, \<one>}"] by (simp add: order_def)
   3.241        have "card {x \<in> carrier (mult_of R). x (^) d = \<one>} \<le> card {x \<in> carrier R. x (^) d = \<one>}"
   3.242          using finite by (auto intro: card_mono)
   3.243 -      also have "\<dots> \<le> d" using `0 < order (mult_of R)` num_roots_le_deg[OF finite, of d]
   3.244 -        by (simp add : dvd_pos_nat[OF _ `d dvd order (mult_of R)`])
   3.245 +      also have "\<dots> \<le> d" using \<open>0 < order (mult_of R)\<close> num_roots_le_deg[OF finite, of d]
   3.246 +        by (simp add : dvd_pos_nat[OF _ \<open>d dvd order (mult_of R)\<close>])
   3.247        finally show ?thesis using G.ord_inj'[OF finite' a] ord_a * by (simp add: card_image)
   3.248      qed
   3.249    qed
   3.250 @@ -811,7 +811,7 @@
   3.251    hence "card ((\<lambda>n. a(^)n) ` {n \<in> {1 .. d}. group.ord (mult_of R) (a(^)n) = d})
   3.252           = card {k \<in> {1 .. d}. group.ord (mult_of R) (a(^)k) = d}"
   3.253           using card_image by blast
   3.254 -  thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' `a \<in> _`, unfolded ord_a]
   3.255 +  thus ?thesis using set_eq2 G.pow_ord_eq_ord_iff[OF finite' \<open>a \<in> _\<close>, unfolded ord_a]
   3.256      by (simp add: phi'_def)
   3.257  qed
   3.258  
     4.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Tue Dec 19 14:51:27 2017 +0100
     4.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Tue Dec 19 13:58:12 2017 +0100
     4.3 @@ -496,7 +496,7 @@
     4.4        cond_application_beta sum.delta' euclidean_representation
     4.5        cong: if_cong)
     4.6  
     4.7 -text \<open>TODO: generalize (via @{text compact_cball})?\<close>
     4.8 +text \<open>TODO: generalize (via \<open>compact_cball\<close>)?\<close>
     4.9  instance blinfun :: (euclidean_space, euclidean_space) heine_borel
    4.10  proof
    4.11    fix f :: "nat \<Rightarrow> 'a \<Rightarrow>\<^sub>L 'b"
     5.1 --- a/src/HOL/Auth/Yahalom.thy	Tue Dec 19 14:51:27 2017 +0100
     5.2 +++ b/src/HOL/Auth/Yahalom.thy	Tue Dec 19 13:58:12 2017 +0100
     5.3 @@ -234,9 +234,9 @@
     5.4  apply (erule yahalom.induct, force,
     5.5         drule_tac [6] YM4_analz_knows_Spy)
     5.6  apply (simp_all add: pushes analz_insert_eq analz_insert_freshK) 
     5.7 -  subgoal --\<open>Fake\<close> by spy_analz
     5.8 -  subgoal --\<open>YM3\<close> by blast   
     5.9 -  subgoal --\<open>Oops\<close> by  (blast dest: unique_session_keys)   
    5.10 +  subgoal \<comment>\<open>Fake\<close> by spy_analz
    5.11 +  subgoal \<comment>\<open>YM3\<close> by blast   
    5.12 +  subgoal \<comment>\<open>Oops\<close> by  (blast dest: unique_session_keys)   
    5.13  done
    5.14  
    5.15  text\<open>Final version\<close>
    5.16 @@ -314,8 +314,8 @@
    5.17  apply (erule yahalom.induct, force,
    5.18         frule_tac [6] YM4_parts_knows_Spy)
    5.19           apply (analz_mono_contra, simp_all)
    5.20 -  subgoal --\<open>Fake\<close> by blast
    5.21 -  subgoal --\<open>YM3\<close> by blast   
    5.22 +  subgoal \<comment>\<open>Fake\<close> by blast
    5.23 +  subgoal \<comment>\<open>YM3\<close> by blast   
    5.24  txt\<open>YM4.  A is uncompromised because NB is secure
    5.25    A's certificate guarantees the existence of the Server message\<close>
    5.26  apply (blast dest!: Gets_imp_Says Crypt_Spy_analz_bad
    5.27 @@ -397,10 +397,10 @@
    5.28    @{term Says_Server_KeyWithNonce}, we get @{prop "~ KeyWithNonce K NB
    5.29    evs"}; then simplification can apply the induction hypothesis with
    5.30    @{term "KK = {K}"}.\<close>
    5.31 -  subgoal --\<open>Fake\<close> by spy_analz
    5.32 -  subgoal --\<open>YM2\<close> by blast
    5.33 -  subgoal --\<open>YM3\<close> by blast
    5.34 -  subgoal --\<open>YM4: If @{prop "A \<in> bad"} then @{term NBa} is known, therefore @{prop "NBa \<noteq> NB"}.\<close>
    5.35 +  subgoal \<comment>\<open>Fake\<close> by spy_analz
    5.36 +  subgoal \<comment>\<open>YM2\<close> by blast
    5.37 +  subgoal \<comment>\<open>YM3\<close> by blast
    5.38 +  subgoal \<comment>\<open>YM4: If @{prop "A \<in> bad"} then @{term NBa} is known, therefore @{prop "NBa \<noteq> NB"}.\<close>
    5.39      by (metis A_trusts_YM3 Gets_imp_analz_Spy Gets_imp_knows_Spy KeyWithNonce_def
    5.40          Spy_analz_shrK analz.Fst analz.Snd analz_shrK_Decrypt parts.Fst parts.Inj)
    5.41  done
    5.42 @@ -484,13 +484,13 @@
    5.43         frule_tac [6] YM4_analz_knows_Spy)
    5.44  apply (simp_all add: split_ifs pushes new_keys_not_analzd analz_insert_eq
    5.45                       analz_insert_freshK)
    5.46 -  subgoal --\<open>Fake\<close> by spy_analz
    5.47 -  subgoal --\<open>YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!\<close> by blast
    5.48 -  subgoal --\<open>YM2\<close> by blast
    5.49 -  subgoal --\<open>YM3: because no NB can also be an NA\<close> 
    5.50 +  subgoal \<comment>\<open>Fake\<close> by spy_analz
    5.51 +  subgoal \<comment>\<open>YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!\<close> by blast
    5.52 +  subgoal \<comment>\<open>YM2\<close> by blast
    5.53 +  subgoal \<comment>\<open>YM3: because no NB can also be an NA\<close> 
    5.54      by (blast dest!: no_nonce_YM1_YM2 dest: Gets_imp_Says Says_unique_NB)
    5.55 -  subgoal --\<open>YM4: key K is visible to Spy, contradicting session key secrecy theorem\<close>
    5.56 -    --\<open>Case analysis on whether Aa is bad;
    5.57 +  subgoal \<comment>\<open>YM4: key K is visible to Spy, contradicting session key secrecy theorem\<close>
    5.58 +    \<comment>\<open>Case analysis on whether Aa is bad;
    5.59              use \<open>Says_unique_NB\<close> to identify message components: @{term "Aa=A"}, @{term "Ba=B"}\<close>
    5.60      apply clarify
    5.61      apply (blast dest!: Says_unique_NB analz_shrK_Decrypt
    5.62 @@ -498,7 +498,7 @@
    5.63                   dest: Gets_imp_Says Says_imp_spies Says_Server_imp_YM2
    5.64                         Spy_not_see_encrypted_key)
    5.65      done
    5.66 -  subgoal --\<open>Oops case: if the nonce is betrayed now, show that the Oops event is
    5.67 +  subgoal \<comment>\<open>Oops case: if the nonce is betrayed now, show that the Oops event is
    5.68      covered by the quantified Oops assumption.\<close>
    5.69      apply clarsimp
    5.70      apply (metis Says_Server_imp_YM2 Gets_imp_Says Says_Server_not_range Says_unique_NB no_nonce_YM1_YM2 parts.Snd single_Nonce_secrecy spies_partsEs(1))
    5.71 @@ -596,10 +596,10 @@
    5.72  apply (erule yahalom.induct, force,
    5.73         frule_tac [6] YM4_parts_knows_Spy)
    5.74  apply (analz_mono_contra, simp_all)
    5.75 -  subgoal --\<open>Fake\<close> by blast
    5.76 -  subgoal --\<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close>
    5.77 +  subgoal \<comment>\<open>Fake\<close> by blast
    5.78 +  subgoal \<comment>\<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close>
    5.79       by (force dest!: Crypt_imp_keysFor)
    5.80 -   subgoal --\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis,
    5.81 +   subgoal \<comment>\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis,
    5.82                 otherwise by unicity of session keys\<close>
    5.83       by (blast dest!: Gets_imp_Says A_trusts_YM3 B_trusts_YM4_shrK Crypt_Spy_analz_bad
    5.84               dest: Says_imp_knows_Spy [THEN parts.Inj] unique_session_keys)
     6.1 --- a/src/HOL/Auth/Yahalom2.thy	Tue Dec 19 14:51:27 2017 +0100
     6.2 +++ b/src/HOL/Auth/Yahalom2.thy	Tue Dec 19 13:58:12 2017 +0100
     6.3 @@ -144,9 +144,9 @@
     6.4  apply (erule rev_mp)
     6.5  apply (erule yahalom.induct, force,
     6.6         frule_tac [6] YM4_parts_knows_Spy, simp_all)
     6.7 -subgoal --\<open>Fake\<close> by (force dest!: keysFor_parts_insert)
     6.8 -subgoal --\<open>YM3 \<close>by blast
     6.9 -subgoal --\<open>YM4\<close> by (fastforce dest!: Gets_imp_knows_Spy [THEN parts.Inj])
    6.10 +subgoal \<comment>\<open>Fake\<close> by (force dest!: keysFor_parts_insert)
    6.11 +subgoal \<comment>\<open>YM3 \<close>by blast
    6.12 +subgoal \<comment>\<open>YM4\<close> by (fastforce dest!: Gets_imp_knows_Spy [THEN parts.Inj])
    6.13  done
    6.14  
    6.15  
    6.16 @@ -400,10 +400,10 @@
    6.17  apply (erule yahalom.induct, force,
    6.18         frule_tac [6] YM4_parts_knows_Spy)
    6.19  apply (analz_mono_contra, simp_all)
    6.20 -  subgoal --\<open>Fake\<close> by blast
    6.21 -  subgoal --\<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close>
    6.22 +  subgoal \<comment>\<open>Fake\<close> by blast
    6.23 +  subgoal \<comment>\<open>YM3 because the message @{term "Crypt K (Nonce NB)"} could not exist\<close>
    6.24      by (force dest!: Crypt_imp_keysFor)
    6.25 -  subgoal --\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis,
    6.26 +  subgoal \<comment>\<open>YM4: was @{term "Crypt K (Nonce NB)"} the very last message? If not, use the induction hypothesis,
    6.27               otherwise by unicity of session keys\<close>
    6.28      by (blast dest!: B_trusts_YM4_shrK dest: secure_unique_session_keys)
    6.29  done
     7.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Tue Dec 19 14:51:27 2017 +0100
     7.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Tue Dec 19 13:58:12 2017 +0100
     7.3 @@ -35,7 +35,7 @@
     7.4  
     7.5  text \<open>
     7.6    If code generation fails with a message like
     7.7 -  @{text \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>},
     7.8 +  \<open>"List.set" is not a constructor, on left hand side of equation: ...\<close>,
     7.9    feel free to add an RBT implementation for the corrsponding operation
    7.10    of delete that code equation (see above).
    7.11  \<close>
     8.1 --- a/src/HOL/Divides.thy	Tue Dec 19 14:51:27 2017 +0100
     8.2 +++ b/src/HOL/Divides.thy	Tue Dec 19 13:58:12 2017 +0100
     8.3 @@ -1327,7 +1327,7 @@
     8.4    then show ?thesis ..
     8.5  qed
     8.6  
     8.7 -lemmas even_times_iff = even_mult_iff -- \<open>FIXME duplicate\<close>
     8.8 +lemmas even_times_iff = even_mult_iff \<comment> \<open>FIXME duplicate\<close>
     8.9  
    8.10  lemma mod_2_not_eq_zero_eq_one_nat:
    8.11    fixes n :: nat
     9.1 --- a/src/HOL/Fun.thy	Tue Dec 19 14:51:27 2017 +0100
     9.2 +++ b/src/HOL/Fun.thy	Tue Dec 19 13:58:12 2017 +0100
     9.3 @@ -154,7 +154,7 @@
     9.4  abbreviation surj :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
     9.5    where "surj f \<equiv> range f = UNIV"
     9.6  
     9.7 -translations -- \<open>The negated case:\<close>
     9.8 +translations \<comment> \<open>The negated case:\<close>
     9.9    "\<not> CONST surj f" \<leftharpoondown> "CONST range f \<noteq> CONST UNIV"
    9.10  
    9.11  abbreviation bij :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"
    10.1 --- a/src/HOL/Power.thy	Tue Dec 19 14:51:27 2017 +0100
    10.2 +++ b/src/HOL/Power.thy	Tue Dec 19 13:58:12 2017 +0100
    10.3 @@ -651,7 +651,7 @@
    10.4  lemma power2_less_0 [simp]: "\<not> a\<^sup>2 < 0"
    10.5    by (force simp add: power2_eq_square mult_less_0_iff)
    10.6  
    10.7 -lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" -- \<open>FIXME simp?\<close>
    10.8 +lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n" \<comment> \<open>FIXME simp?\<close>
    10.9    by (induct n) (simp_all add: abs_mult)
   10.10  
   10.11  lemma power_sgn [simp]: "sgn (a ^ n) = sgn a ^ n"
    11.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Dec 19 14:51:27 2017 +0100
    11.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Tue Dec 19 13:58:12 2017 +0100
    11.3 @@ -125,7 +125,7 @@
    11.4  
    11.5  code_pred predicate_where_argument_is_neg_condition_and_in_equation .
    11.6  
    11.7 -text {* Another related example that required slight adjustment of the proof procedure *}
    11.8 +text \<open>Another related example that required slight adjustment of the proof procedure\<close>
    11.9  
   11.10  inductive if_as_predicate :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   11.11  where
    12.1 --- a/src/HOL/Probability/Conditional_Expectation.thy	Tue Dec 19 14:51:27 2017 +0100
    12.2 +++ b/src/HOL/Probability/Conditional_Expectation.thy	Tue Dec 19 13:58:12 2017 +0100
    12.3 @@ -8,7 +8,7 @@
    12.4  imports Probability_Measure
    12.5  begin
    12.6  
    12.7 -subsection {*Restricting a measure to a sub-sigma-algebra*}
    12.8 +subsection \<open>Restricting a measure to a sub-sigma-algebra\<close>
    12.9  
   12.10  definition subalgebra::"'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
   12.11    "subalgebra M F = ((space F = space M) \<and> (sets F \<subseteq> sets M))"
   12.12 @@ -83,7 +83,7 @@
   12.13    then have "U \<in> sets F" by simp
   12.14    then have "U \<in> sets M" using assms(1) by (meson subalgebra_def subsetD)
   12.15    then have "U \<in> null_sets M" unfolding U_def using assms(2) using AE_iff_measurable by blast
   12.16 -  then have "U \<in> null_sets (restr_to_subalg M F)" using null_sets_restr_to_subalg[OF assms(1)] `U \<in> sets F` by auto
   12.17 +  then have "U \<in> null_sets (restr_to_subalg M F)" using null_sets_restr_to_subalg[OF assms(1)] \<open>U \<in> sets F\<close> by auto
   12.18    then show ?thesis using * by (metis (no_types, lifting) Collect_mono U_def eventually_ae_filter space_restr_to_subalg)
   12.19  qed
   12.20  
   12.21 @@ -119,9 +119,9 @@
   12.22    shows "f \<in> measurable M N"
   12.23  using assms unfolding measurable_def subalgebra_def by auto
   12.24  
   12.25 -text{*The following is the direct transposition of \verb+nn_integral_subalgebra+
   12.26 +text\<open>The following is the direct transposition of \verb+nn_integral_subalgebra+
   12.27  (from \verb+Nonnegative_Lebesgue_Integration+) in the
   12.28 -current notations, with the removal of the useless assumption $f \geq 0$.*}
   12.29 +current notations, with the removal of the useless assumption $f \geq 0$.\<close>
   12.30  
   12.31  lemma nn_integral_subalgebra2:
   12.32    assumes "subalgebra M F" and [measurable]: "f \<in> borel_measurable F"
   12.33 @@ -135,8 +135,8 @@
   12.34      by (metis sets_restr_to_subalg[OF assms(1)] emeasure_restr_to_subalg[OF assms(1)])
   12.35  qed (auto simp add: assms space_restr_to_subalg sets_restr_to_subalg[OF assms(1)])
   12.36  
   12.37 -text{*The following is the direct transposition of \verb+integral_subalgebra+
   12.38 -(from \verb+Bochner_Integration+) in the current notations.*}
   12.39 +text\<open>The following is the direct transposition of \verb+integral_subalgebra+
   12.40 +(from \verb+Bochner_Integration+) in the current notations.\<close>
   12.41  
   12.42  lemma integral_subalgebra2:
   12.43    fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   12.44 @@ -177,9 +177,9 @@
   12.45    finally show "(\<integral>\<^sup>+ x. ennreal (norm (f x)) \<partial>(restr_to_subalg M F)) < \<infinity>" by simp
   12.46  qed
   12.47  
   12.48 -subsection {*Nonnegative conditional expectation*}
   12.49 +subsection \<open>Nonnegative conditional expectation\<close>
   12.50  
   12.51 -text {* The conditional expectation of a function $f$, on a measure space $M$, with respect to a
   12.52 +text \<open>The conditional expectation of a function $f$, on a measure space $M$, with respect to a
   12.53  sub sigma algebra $F$, should be a function $g$ which is $F$-measurable whose integral on any
   12.54  $F$-set coincides with the integral of $f$.
   12.55  Such a function is uniquely defined almost everywhere.
   12.56 @@ -192,7 +192,7 @@
   12.57  In this paragraph, we develop the definition and basic properties for nonnegative functions,
   12.58  as the basics of the general case. As in the definition of integrals, the nonnegative case is done
   12.59  with ennreal-valued functions, without any integrability assumption.
   12.60 -*}
   12.61 +\<close>
   12.62  
   12.63  definition nn_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ('a \<Rightarrow> ennreal)"
   12.64  where
   12.65 @@ -207,11 +207,11 @@
   12.66  by (simp_all add: nn_cond_exp_def)
   12.67    (metis borel_measurable_RN_deriv borel_measurable_subalgebra sets_restr_to_subalg space_restr_to_subalg subalgebra_def)
   12.68  
   12.69 -text {* The good setting for conditional expectations is the situation where the subalgebra $F$
   12.70 +text \<open>The good setting for conditional expectations is the situation where the subalgebra $F$
   12.71  gives rise to a sigma-finite measure space. To see what goes wrong if it is not sigma-finite,
   12.72  think of $\mathbb{R}$ with the trivial sigma-algebra $\{\emptyset, \mathbb{R}\}$. In this case,
   12.73  conditional expectations have to be constant functions, so they have integral $0$ or $\infty$.
   12.74 -This means that a positive integrable function can have no meaningful conditional expectation.*}
   12.75 +This means that a positive integrable function can have no meaningful conditional expectation.\<close>
   12.76  
   12.77  locale sigma_finite_subalgebra =
   12.78    fixes M F::"'a measure"
   12.79 @@ -230,15 +230,15 @@
   12.80    have "A \<subseteq> sets F" using Ap sets_restr_to_subalg[OF subalg] by fastforce
   12.81    then have "A \<subseteq> sets M" using subalg subalgebra_def by force
   12.82    moreover have "\<Union>A = space M" using Ap space_restr_to_subalg by simp
   12.83 -  moreover have "\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>" by (metis subsetD emeasure_restr_to_subalg[OF subalg] `A \<subseteq> sets F` Ap)
   12.84 +  moreover have "\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>" by (metis subsetD emeasure_restr_to_subalg[OF subalg] \<open>A \<subseteq> sets F\<close> Ap)
   12.85    ultimately show "\<exists>A. countable A \<and> A \<subseteq> sets M \<and> \<Union>A = space M \<and> (\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>)" using Ap by auto
   12.86  qed
   12.87  
   12.88  sublocale sigma_finite_subalgebra \<subseteq> sigma_finite_measure
   12.89  using sigma_finite_subalgebra_is_sigma_finite sigma_finite_subalgebra_axioms by blast
   12.90  
   12.91 -text {* Conditional expectations are very often used in probability spaces. This is a special case
   12.92 -of the previous one, as we prove now. *}
   12.93 +text \<open>Conditional expectations are very often used in probability spaces. This is a special case
   12.94 +of the previous one, as we prove now.\<close>
   12.95  
   12.96  locale finite_measure_subalgebra = finite_measure +
   12.97    fixes F::"'a measure"
   12.98 @@ -268,14 +268,14 @@
   12.99  context sigma_finite_subalgebra
  12.100  begin
  12.101  
  12.102 -text{* The next lemma is arguably the most fundamental property of conditional expectation:
  12.103 +text\<open>The next lemma is arguably the most fundamental property of conditional expectation:
  12.104  when computing an expectation against an $F$-measurable function, it is equivalent to work
  12.105  with a function or with its $F$-conditional expectation.
  12.106  
  12.107  This property (even for bounded test functions) characterizes conditional expectations, as the second lemma below shows.
  12.108  From this point on, we will only work with it, and forget completely about
  12.109  the definition using Radon-Nikodym derivatives.
  12.110 -*}
  12.111 +\<close>
  12.112  
  12.113  lemma nn_cond_exp_intg:
  12.114    assumes [measurable]: "f \<in> borel_measurable F" "g \<in> borel_measurable M"
  12.115 @@ -371,7 +371,7 @@
  12.116    fix A assume [measurable]: "A \<in> sets F"
  12.117    then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
  12.118    have "\<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M = (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. nn_cond_exp M F g x \<partial>M)"
  12.119 -    by (rule nn_set_integral_add) (auto simp add: assms `A \<in> sets M`)
  12.120 +    by (rule nn_set_integral_add) (auto simp add: assms \<open>A \<in> sets M\<close>)
  12.121    also have "... = (\<integral>\<^sup>+x. indicator A x * nn_cond_exp M F f x \<partial>M) + (\<integral>\<^sup>+x. indicator A x * nn_cond_exp M F g x \<partial>M)"
  12.122      by (metis (no_types, lifting) mult.commute nn_integral_cong)
  12.123    also have "... = (\<integral>\<^sup>+x. indicator A x * f x \<partial>M) + (\<integral>\<^sup>+x. indicator A x * g x \<partial>M)"
  12.124 @@ -379,7 +379,7 @@
  12.125    also have "... = (\<integral>\<^sup>+x\<in>A. f x \<partial>M) + (\<integral>\<^sup>+x\<in>A. g x \<partial>M)"
  12.126      by (metis (no_types, lifting) mult.commute nn_integral_cong)
  12.127    also have "... = \<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M"
  12.128 -    by (rule nn_set_integral_add[symmetric]) (auto simp add: assms `A \<in> sets M`)
  12.129 +    by (rule nn_set_integral_add[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close>)
  12.130    finally show "\<integral>\<^sup>+x\<in>A. (f x + g x)\<partial>M = \<integral>\<^sup>+x\<in>A. (nn_cond_exp M F f x + nn_cond_exp M F g x)\<partial>M"
  12.131      by simp
  12.132  qed (auto simp add: assms)
  12.133 @@ -450,14 +450,14 @@
  12.134  
  12.135  end
  12.136  
  12.137 -subsection {*Real conditional expectation*}
  12.138 +subsection \<open>Real conditional expectation\<close>
  12.139  
  12.140 -text {*Once conditional expectations of positive functions are defined, the definition for real-valued functions
  12.141 +text \<open>Once conditional expectations of positive functions are defined, the definition for real-valued functions
  12.142  follows readily, by taking the difference of positive and negative parts.
  12.143  One could also define a conditional expectation of vector-space valued functions, as in
  12.144  \verb+Bochner_Integral+, but since the real-valued case is the most important, and quicker to formalize, I
  12.145  concentrate on it. (It is also essential for the case of the most general Pettis integral.)
  12.146 -*}
  12.147 +\<close>
  12.148  
  12.149  definition real_cond_exp :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real)" where
  12.150    "real_cond_exp M F f =
  12.151 @@ -497,7 +497,7 @@
  12.152    then show ?thesis using eq by simp
  12.153  qed
  12.154  
  12.155 -text{* The next lemma shows that the conditional expectation
  12.156 +text\<open>The next lemma shows that the conditional expectation
  12.157  is an $F$-measurable function whose average against an $F$-measurable
  12.158  function $f$ coincides with the average of the original function against $f$.
  12.159  It is obtained as a consequence of the same property for the positive conditional
  12.160 @@ -511,7 +511,7 @@
  12.161  Once this lemma is available, we will use it to characterize the conditional expectation,
  12.162  and never come back to the original technical definition, as we did in the case of the
  12.163  nonnegative conditional expectation.
  12.164 -*}
  12.165 +\<close>
  12.166  
  12.167  lemma real_cond_exp_intg_fpos:
  12.168    assumes "integrable M (\<lambda>x. f x * g x)" and f_pos[simp]: "\<And>x. f x \<ge> 0" and
  12.169 @@ -738,7 +738,7 @@
  12.170    shows "(\<integral> x \<in> A. f x \<partial>M) = (\<integral>x \<in> A. real_cond_exp M F f x \<partial>M)"
  12.171  proof -
  12.172    have "A \<in> sets M" by (meson assms(2) subalg subalgebra_def subsetD)
  12.173 -  have "integrable M (\<lambda>x. indicator A x * f x)" using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
  12.174 +  have "integrable M (\<lambda>x. indicator A x * f x)" using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
  12.175    then show ?thesis using real_cond_exp_intg(2)[where ?f = "indicator A" and ?g = f, symmetric] by auto
  12.176  qed
  12.177  
  12.178 @@ -789,12 +789,12 @@
  12.179  proof (rule real_cond_exp_charact)
  12.180    fix A assume "A \<in> sets F"
  12.181    then have [measurable]: "(\<lambda>x. f x * indicator A x) \<in> borel_measurable F" by measurable
  12.182 -  have [measurable]: "A \<in> sets M" using subalg by (meson `A \<in> sets F` subalgebra_def subsetD)
  12.183 +  have [measurable]: "A \<in> sets M" using subalg by (meson \<open>A \<in> sets F\<close> subalgebra_def subsetD)
  12.184    have "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x. (f x * indicator A x) * g x \<partial>M"
  12.185      by (simp add: mult.commute mult.left_commute)
  12.186    also have "... = \<integral>x. (f x * indicator A x) * real_cond_exp M F g x \<partial>M"
  12.187      apply (rule real_cond_exp_intg(2)[symmetric], auto simp add: assms)
  12.188 -    using integrable_mult_indicator[OF `A \<in> sets M` assms(3)] by (simp add: mult.commute mult.left_commute)
  12.189 +    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(3)] by (simp add: mult.commute mult.left_commute)
  12.190    also have "... = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M"
  12.191      by (simp add: mult.commute mult.left_commute)
  12.192    finally show "\<integral>x\<in>A. (f x * g x) \<partial>M = \<integral>x\<in>A. (f x * real_cond_exp M F g x)\<partial>M" by simp
  12.193 @@ -812,22 +812,22 @@
  12.194    fix A assume [measurable]: "A \<in> sets F"
  12.195    then have "A \<in> sets M" by (meson subalg subalgebra_def subsetD)
  12.196    have intAf: "integrable M (\<lambda>x. indicator A x * f x)"
  12.197 -    using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
  12.198 +    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
  12.199    have intAg: "integrable M (\<lambda>x. indicator A x * g x)"
  12.200 -    using integrable_mult_indicator[OF `A \<in> sets M` assms(2)] by auto
  12.201 +    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(2)] by auto
  12.202  
  12.203    have "\<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M) + (\<integral>x\<in>A. real_cond_exp M F g x \<partial>M)"
  12.204      apply (rule set_integral_add, auto simp add: assms)
  12.205 -    using integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(1)]]
  12.206 -          integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(2)]] by simp_all
  12.207 +    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]]
  12.208 +          integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(2)]] by simp_all
  12.209    also have "... = (\<integral>x. indicator A x * real_cond_exp M F f x \<partial>M) + (\<integral>x. indicator A x * real_cond_exp M F g x \<partial>M)"
  12.210      by auto
  12.211    also have "... = (\<integral>x. indicator A x * f x \<partial>M) + (\<integral>x. indicator A x * g x \<partial>M)"
  12.212 -    using real_cond_exp_intg(2) assms `A \<in> sets F` intAf intAg by auto
  12.213 +    using real_cond_exp_intg(2) assms \<open>A \<in> sets F\<close> intAf intAg by auto
  12.214    also have "... = (\<integral>x\<in>A. f x \<partial>M) + (\<integral>x\<in>A. g x \<partial>M)"
  12.215      by auto
  12.216    also have "... = \<integral>x\<in>A. (f x + g x)\<partial>M"
  12.217 -    by (rule set_integral_add(2)[symmetric]) (auto simp add: assms `A \<in> sets M` intAf intAg)
  12.218 +    by (rule set_integral_add(2)[symmetric]) (auto simp add: assms \<open>A \<in> sets M\<close> intAf intAg)
  12.219    finally show "\<integral>x\<in>A. (f x + g x)\<partial>M = \<integral>x\<in>A. (real_cond_exp M F f x + real_cond_exp M F g x)\<partial>M"
  12.220      by simp
  12.221  qed (auto simp add: assms)
  12.222 @@ -924,7 +924,7 @@
  12.223      have "emeasure (restr_to_subalg M F) X = emeasure M X"
  12.224        by (simp add: emeasure_restr_to_subalg subalg)
  12.225      then have "emeasure (restr_to_subalg M F) X > 0"
  12.226 -      using `\<not>(emeasure M X) = 0` gr_zeroI by auto
  12.227 +      using \<open>\<not>(emeasure M X) = 0\<close> gr_zeroI by auto
  12.228      then obtain A where "A \<in> sets (restr_to_subalg M F)" "A \<subseteq> X" "emeasure (restr_to_subalg M F) A > 0" "emeasure (restr_to_subalg M F) A < \<infinity>"
  12.229        using sigma_fin_subalg by (metis emeasure_notin_sets ennreal_0 infinity_ennreal_def le_less_linear neq_top_trans
  12.230        not_gr_zero order_refl sigma_finite_measure.approx_PInf_emeasure_with_finite)
  12.231 @@ -933,16 +933,16 @@
  12.232      have Ic: "set_integrable M A (\<lambda>x. c)"
  12.233        using \<open>emeasure (restr_to_subalg M F) A < \<infinity>\<close> emeasure_restr_to_subalg subalg by fastforce
  12.234      have If: "set_integrable M A f"
  12.235 -      by (rule integrable_mult_indicator, auto simp add: `integrable M f`)
  12.236 +      by (rule integrable_mult_indicator, auto simp add: \<open>integrable M f\<close>)
  12.237      have *: "(\<integral>x\<in>A. c \<partial>M) = (\<integral>x\<in>A. f x \<partial>M)"
  12.238      proof (rule antisym)
  12.239        show "(\<integral>x\<in>A. c \<partial>M) \<le> (\<integral>x\<in>A. f x \<partial>M)"
  12.240          apply (rule set_integral_mono_AE) using Ic If assms(2) by auto
  12.241        have "(\<integral>x\<in>A. f x \<partial>M) = (\<integral>x\<in>A. real_cond_exp M F f x \<partial>M)"
  12.242 -        by (rule real_cond_exp_intA, auto simp add: `integrable M f`)
  12.243 +        by (rule real_cond_exp_intA, auto simp add: \<open>integrable M f\<close>)
  12.244        also have "... \<le> (\<integral>x\<in>A. c \<partial>M)"
  12.245          apply (rule set_integral_mono)
  12.246 -        apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF `integrable M f`])
  12.247 +        apply (rule integrable_mult_indicator, simp, simp add: real_cond_exp_int(1)[OF \<open>integrable M f\<close>])
  12.248          using Ic X_def \<open>A \<subseteq> X\<close> by auto
  12.249        finally show "(\<integral>x\<in>A. f x \<partial>M) \<le> (\<integral>x\<in>A. c \<partial>M)" by simp
  12.250      qed
  12.251 @@ -952,10 +952,10 @@
  12.252      then have "AE x\<in>A in M. c = f x" by auto
  12.253      then have "AE x\<in>A in M. False" using assms(2) by auto
  12.254      have "A \<in> null_sets M" unfolding ae_filter_def by (meson AE_iff_null_sets \<open>A \<in> sets M\<close> \<open>AE x\<in>A in M. False\<close>)
  12.255 -    then show False using `emeasure (restr_to_subalg M F) A > 0`
  12.256 +    then show False using \<open>emeasure (restr_to_subalg M F) A > 0\<close>
  12.257        by (simp add: emeasure_restr_to_subalg null_setsD1 subalg)
  12.258    qed
  12.259 -  then show ?thesis using AE_iff_null_sets[OF `X \<in> sets M`] unfolding X_def by auto
  12.260 +  then show ?thesis using AE_iff_null_sets[OF \<open>X \<in> sets M\<close>] unfolding X_def by auto
  12.261  qed
  12.262  
  12.263  lemma real_cond_exp_less_c:
  12.264 @@ -964,7 +964,7 @@
  12.265    shows "AE x in M. real_cond_exp M F f x < c"
  12.266  proof -
  12.267    have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (\<lambda>x. -f x) x"
  12.268 -    using real_cond_exp_cmult[OF `integrable M f`, of "-1"] by auto
  12.269 +    using real_cond_exp_cmult[OF \<open>integrable M f\<close>, of "-1"] by auto
  12.270    moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -f x) x > -c"
  12.271      apply (rule real_cond_exp_gr_c) using assms by auto
  12.272    ultimately show ?thesis by auto
  12.273 @@ -978,7 +978,7 @@
  12.274    obtain u::"nat \<Rightarrow> real" where u: "\<And>n. u n < c" "u \<longlonglongrightarrow> c"
  12.275      using approx_from_below_dense_linorder[of "c-1" c] by auto
  12.276    have *: "AE x in M. real_cond_exp M F f x > u n" for n::nat
  12.277 -    apply (rule real_cond_exp_gr_c) using assms `u n < c` by auto
  12.278 +    apply (rule real_cond_exp_gr_c) using assms \<open>u n < c\<close> by auto
  12.279    have "AE x in M. \<forall>n. real_cond_exp M F f x > u n"
  12.280      by (subst AE_all_countable, auto simp add: *)
  12.281    moreover have "real_cond_exp M F f x \<ge> c" if "\<forall>n. real_cond_exp M F f x > u n" for x
  12.282 @@ -995,7 +995,7 @@
  12.283    shows "AE x in M. real_cond_exp M F f x \<le> c"
  12.284  proof -
  12.285    have "AE x in M. real_cond_exp M F f x = -real_cond_exp M F (\<lambda>x. -f x) x"
  12.286 -    using real_cond_exp_cmult[OF `integrable M f`, of "-1"] by auto
  12.287 +    using real_cond_exp_cmult[OF \<open>integrable M f\<close>, of "-1"] by auto
  12.288    moreover have "AE x in M. real_cond_exp M F (\<lambda>x. -f x) x \<ge> -c"
  12.289      apply (rule real_cond_exp_ge_c) using assms by auto
  12.290    ultimately show ?thesis by auto
  12.291 @@ -1038,9 +1038,9 @@
  12.292    fix A assume [measurable]: "A \<in> sets F"
  12.293    then have A_meas [measurable]: "A \<in> sets M" by (meson set_mp subalg subalgebra_def)
  12.294    have *: "integrable M (\<lambda>x. indicator A x * f i x)" for i
  12.295 -    using integrable_mult_indicator[OF `A \<in> sets M` assms(1)] by auto
  12.296 +    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> assms(1)] by auto
  12.297    have **: "integrable M (\<lambda>x. indicator A x * real_cond_exp M F (f i) x)" for i
  12.298 -    using integrable_mult_indicator[OF `A \<in> sets M` real_cond_exp_int(1)[OF assms(1)]] by auto
  12.299 +    using integrable_mult_indicator[OF \<open>A \<in> sets M\<close> real_cond_exp_int(1)[OF assms(1)]] by auto
  12.300    have inti: "(\<integral>x. indicator A x * f i x \<partial>M) = (\<integral>x. indicator A x * real_cond_exp M F (f i) x \<partial>M)" for i
  12.301      by (rule real_cond_exp_intg(2)[symmetric], auto simp add: *)
  12.302  
  12.303 @@ -1057,8 +1057,8 @@
  12.304    finally show "(\<integral>x\<in>A. (\<Sum>i\<in>I. f i x)\<partial>M) = (\<integral>x\<in>A. (\<Sum>i\<in>I. real_cond_exp M F (f i) x)\<partial>M)" by auto
  12.305  qed (auto simp add: assms real_cond_exp_int(1)[OF assms(1)])
  12.306  
  12.307 -text {*Jensen's inequality, describing the behavior of the integral under a convex function, admits
  12.308 -a version for the conditional expectation, as follows.*}
  12.309 +text \<open>Jensen's inequality, describing the behavior of the integral under a convex function, admits
  12.310 +a version for the conditional expectation, as follows.\<close>
  12.311  
  12.312  theorem real_cond_exp_jensens_inequality:
  12.313    fixes q :: "real \<Rightarrow> real"
  12.314 @@ -1075,14 +1075,14 @@
  12.315    have **: "q (X x) \<ge> q (real_cond_exp M F X x) + phi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)"
  12.316          if "X x \<in> I" "real_cond_exp M F X x \<in> I" for x
  12.317      unfolding phi_def apply (rule convex_le_Inf_differential)
  12.318 -    using `convex_on I q` that `interior I = I` by auto
  12.319 -  text {*It is not clear that the function $\phi$ is measurable. We replace it by a version which
  12.320 -        is better behaved.*}
  12.321 +    using \<open>convex_on I q\<close> that \<open>interior I = I\<close> by auto
  12.322 +  text \<open>It is not clear that the function $\phi$ is measurable. We replace it by a version which
  12.323 +        is better behaved.\<close>
  12.324    define psi where "psi = (\<lambda>x. phi x * indicator I x)"
  12.325    have A: "psi y = phi y" if "y \<in> I" for y unfolding psi_def indicator_def using that by auto
  12.326    have *: "q (X x) \<ge> q (real_cond_exp M F X x) + psi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)"
  12.327          if "X x \<in> I" "real_cond_exp M F X x \<in> I" for x
  12.328 -    unfolding A[OF `real_cond_exp M F X x \<in> I`] using ** that by auto
  12.329 +    unfolding A[OF \<open>real_cond_exp M F X x \<in> I\<close>] using ** that by auto
  12.330  
  12.331    note I
  12.332    moreover have "AE x in M. real_cond_exp M F X x > a" if "I \<subseteq> {a <..}" for a
  12.333 @@ -1094,12 +1094,12 @@
  12.334    then have main_ineq: "AE x in M. q (X x) \<ge> q (real_cond_exp M F X x) + psi (real_cond_exp M F X x) * (X x - real_cond_exp M F X x)"
  12.335      using * X(2) by auto
  12.336  
  12.337 -  text {*Then, one wants to take the conditional expectation of this inequality. On the left, one gets
  12.338 +  text \<open>Then, one wants to take the conditional expectation of this inequality. On the left, one gets
  12.339           the conditional expectation of $q \circ X$. On the right, the last term vanishes, and one
  12.340           is left with $q$ of the conditional expectation, as desired. Unfortunately, this argument only
  12.341           works if $\psi \cdot X$ and $q(E(X | F))$ are integrable, and there is no reason why this should be true. The
  12.342           trick is to multiply by a $F$-measurable function which is small enough to make
  12.343 -         everything integrable.*}
  12.344 +         everything integrable.\<close>
  12.345  
  12.346    obtain f::"'a \<Rightarrow> real" where [measurable]: "f \<in> borel_measurable (restr_to_subalg M F)"
  12.347                                 "integrable (restr_to_subalg M F) f"
  12.348 @@ -1123,31 +1123,31 @@
  12.349    then have main_G: "AE x in M. g x * q (X x) \<ge> g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)"
  12.350      unfolding G_def by (auto simp add: algebra_simps)
  12.351  
  12.352 -  text {*To proceed, we need to know that $\psi$ is measurable.*}
  12.353 +  text \<open>To proceed, we need to know that $\psi$ is measurable.\<close>
  12.354    have phi_mono: "phi x \<le> phi y" if "x \<le> y" "x \<in> I" "y \<in> I" for x y
  12.355    proof (cases "x < y")
  12.356      case True
  12.357      have "q x + phi x * (y-x) \<le> q y"
  12.358 -      unfolding phi_def apply (rule convex_le_Inf_differential) using `convex_on I q` that `interior I = I` by auto
  12.359 +      unfolding phi_def apply (rule convex_le_Inf_differential) using \<open>convex_on I q\<close> that \<open>interior I = I\<close> by auto
  12.360      then have "phi x \<le> (q x - q y) / (x - y)"
  12.361 -      using that `x < y` by (auto simp add: divide_simps algebra_simps)
  12.362 +      using that \<open>x < y\<close> by (auto simp add: divide_simps algebra_simps)
  12.363      moreover have "(q x - q y)/(x - y) \<le> phi y"
  12.364      unfolding phi_def proof (rule cInf_greatest, auto)
  12.365        fix t assume "t \<in> I" "y < t"
  12.366        have "(q x - q y) / (x - y) \<le> (q x - q t) / (x - t)"
  12.367 -        apply (rule convex_on_diff[OF q(2)]) using `y < t` `x < y` `t \<in> I` `x \<in> I` by auto
  12.368 +        apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
  12.369        also have "... \<le> (q y - q t) / (y - t)"
  12.370 -        apply (rule convex_on_diff[OF q(2)]) using `y < t` `x < y` `t \<in> I` `x \<in> I` by auto
  12.371 +        apply (rule convex_on_diff[OF q(2)]) using \<open>y < t\<close> \<open>x < y\<close> \<open>t \<in> I\<close> \<open>x \<in> I\<close> by auto
  12.372        finally show "(q x - q y) / (x - y) \<le> (q y - q t) / (y - t)" by simp
  12.373      next
  12.374 -      obtain e where "0 < e" "ball y e \<subseteq> I" using `open I` `y \<in> I` openE by blast
  12.375 +      obtain e where "0 < e" "ball y e \<subseteq> I" using \<open>open I\<close> \<open>y \<in> I\<close> openE by blast
  12.376        then have "y + e/2 \<in> {y<..} \<inter> I" by (auto simp: dist_real_def)
  12.377        then show "{y<..} \<inter> I = {} \<Longrightarrow> False" by auto
  12.378      qed
  12.379      ultimately show "phi x \<le> phi y" by auto
  12.380    next
  12.381      case False
  12.382 -    then have "x = y" using `x \<le> y` by auto
  12.383 +    then have "x = y" using \<open>x \<le> y\<close> by auto
  12.384      then show ?thesis by auto
  12.385    qed
  12.386    have [measurable]: "psi \<in> borel_measurable borel"
  12.387 @@ -1161,27 +1161,27 @@
  12.388                       "G \<in> borel_measurable F" "G \<in> borel_measurable M"
  12.389      using X measurable_from_subalg[OF subalg] unfolding G_def g_def by auto
  12.390    have int1: "integrable (restr_to_subalg M F) (\<lambda>x. g x * q (real_cond_exp M F X x))"
  12.391 -    apply (rule Bochner_Integration.integrable_bound[of _ f], auto simp add: subalg `integrable (restr_to_subalg M F) f`)
  12.392 +    apply (rule Bochner_Integration.integrable_bound[of _ f], auto simp add: subalg \<open>integrable (restr_to_subalg M F) f\<close>)
  12.393      unfolding g_def by (auto simp add: divide_simps abs_mult algebra_simps)
  12.394    have int2: "integrable M (\<lambda>x. G x * (X x - real_cond_exp M F X x))"
  12.395      apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. \<bar>X x\<bar> + \<bar>real_cond_exp M F X x\<bar>"])
  12.396 -    apply (auto intro!: Bochner_Integration.integrable_add integrable_abs real_cond_exp_int `integrable M X` AE_I2)
  12.397 +    apply (auto intro!: Bochner_Integration.integrable_add integrable_abs real_cond_exp_int \<open>integrable M X\<close> AE_I2)
  12.398      using G unfolding abs_mult by (meson abs_ge_zero abs_triangle_ineq4 dual_order.trans mult_left_le_one_le)
  12.399    have int3: "integrable M (\<lambda>x. g x * q (X x))"
  12.400      apply (rule Bochner_Integration.integrable_bound[of _ "\<lambda>x. q(X x)"], auto simp add: q(1) abs_mult)
  12.401      using g by (simp add: less_imp_le mult_left_le_one_le)
  12.402  
  12.403 -  text {*Taking the conditional expectation of the main convexity inequality \verb+main_G+, we get
  12.404 -         the following.*}
  12.405 +  text \<open>Taking the conditional expectation of the main convexity inequality \verb+main_G+, we get
  12.406 +         the following.\<close>
  12.407    have "AE x in M. real_cond_exp M F (\<lambda>x. g x * q (X x)) x \<ge> real_cond_exp M F (\<lambda>x. g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)) x"
  12.408      apply (rule real_cond_exp_mono[OF main_G])
  12.409      apply (rule Bochner_Integration.integrable_add[OF integrable_from_subalg[OF subalg int1]])
  12.410      using int2 int3 by auto
  12.411 -  text {*This reduces to the desired inequality thanks to the properties of conditional expectation,
  12.412 +  text \<open>This reduces to the desired inequality thanks to the properties of conditional expectation,
  12.413           i.e., the conditional expectation of an $F$-measurable function is this function, and one can
  12.414           multiply an $F$-measurable function outside of conditional expectations.
  12.415           Since all these equalities only hold almost everywhere, we formulate them separately,
  12.416 -         and then combine all of them to simplify the above equation, again almost everywhere.*}
  12.417 +         and then combine all of them to simplify the above equation, again almost everywhere.\<close>
  12.418    moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x * q (X x)) x = g x * real_cond_exp M F (\<lambda>x. q (X x)) x"
  12.419      by (rule real_cond_exp_mult, auto simp add: int3)
  12.420    moreover have "AE x in M. real_cond_exp M F (\<lambda>x. g x * q (real_cond_exp M F X x) + G x * (X x - real_cond_exp M F X x)) x
  12.421 @@ -1192,16 +1192,16 @@
  12.422    moreover have "AE x in M. real_cond_exp M F (\<lambda>x. G x * (X x - real_cond_exp M F X x)) x = G x * real_cond_exp M F (\<lambda>x. (X x - real_cond_exp M F X x)) x"
  12.423      by (rule real_cond_exp_mult, auto simp add: int2)
  12.424    moreover have "AE x in M. real_cond_exp M F (\<lambda>x. (X x - real_cond_exp M F X x)) x = real_cond_exp M F X x - real_cond_exp M F (\<lambda>x. real_cond_exp M F X x) x"
  12.425 -    by (rule real_cond_exp_diff, auto intro!: real_cond_exp_int `integrable M X`)
  12.426 +    by (rule real_cond_exp_diff, auto intro!: real_cond_exp_int \<open>integrable M X\<close>)
  12.427    moreover have "AE x in M. real_cond_exp M F (\<lambda>x. real_cond_exp M F X x) x = real_cond_exp M F X x "
  12.428 -    by (rule real_cond_exp_F_meas, auto intro!: real_cond_exp_int `integrable M X`)
  12.429 +    by (rule real_cond_exp_F_meas, auto intro!: real_cond_exp_int \<open>integrable M X\<close>)
  12.430    ultimately have "AE x in M. g x * real_cond_exp M F (\<lambda>x. q (X x)) x \<ge> g x * q (real_cond_exp M F X x)"
  12.431      by auto
  12.432    then show "AE x in M. real_cond_exp M F (\<lambda>x. q (X x)) x \<ge> q (real_cond_exp M F X x)"
  12.433      using g(1) by (auto simp add: divide_simps)
  12.434  qed
  12.435  
  12.436 -text {*Jensen's inequality does not imply that $q(E(X|F))$ is integrable, as it only proves an upper
  12.437 +text \<open>Jensen's inequality does not imply that $q(E(X|F))$ is integrable, as it only proves an upper
  12.438  bound for it. Indeed, this is not true in general, as the following counterexample shows:
  12.439  
  12.440  on $[1,\infty)$ with Lebesgue measure, let $F$ be the sigma-algebra generated by the intervals $[n, n+1)$
  12.441 @@ -1214,7 +1214,7 @@
  12.442  
  12.443  However, this counterexample is essentially the only situation where this function is not
  12.444  integrable, as shown by the next lemma.
  12.445 -*}
  12.446 +\<close>
  12.447  
  12.448  lemma integrable_convex_cond_exp:
  12.449    fixes q :: "real \<Rightarrow> real"
  12.450 @@ -1242,12 +1242,12 @@
  12.451      interpret finite_measure M using 2 by (auto intro!: finite_measureI)
  12.452  
  12.453      have "I \<noteq> {}"
  12.454 -      using `AE x in M. X x \<in> I` 2 eventually_mono integral_less_AE_space by fastforce
  12.455 +      using \<open>AE x in M. X x \<in> I\<close> 2 eventually_mono integral_less_AE_space by fastforce
  12.456      then obtain z where "z \<in> I" by auto
  12.457  
  12.458      define A where "A = Inf ((\<lambda>t. (q z - q t) / (z - t)) ` ({z<..} \<inter> I))"
  12.459      have "q y \<ge> q z + A * (y - z)" if "y \<in> I" for y unfolding A_def apply (rule convex_le_Inf_differential)
  12.460 -      using `z \<in> I` `y \<in> I` `interior I = I` q(2) by auto
  12.461 +      using \<open>z \<in> I\<close> \<open>y \<in> I\<close> \<open>interior I = I\<close> q(2) by auto
  12.462      then have "AE x in M. q (real_cond_exp M F X x) \<ge> q z + A * (real_cond_exp M F X x - z)"
  12.463        using real_cond_exp_jensens_inequality(1)[OF X I q] by auto
  12.464      moreover have "AE x in M. q (real_cond_exp M F X x) \<le> real_cond_exp M F (\<lambda>x. q (X x)) x"
  12.465 @@ -1271,8 +1271,8 @@
  12.466        define e where "e = \<bar>q(0)\<bar> / 2"
  12.467        then have "e > 0" using * by auto
  12.468        have "continuous (at 0) q"
  12.469 -        using q(2) `0 \<in> I` `open I` \<open>interior I = I\<close> continuous_on_interior convex_on_continuous by blast
  12.470 -      then obtain d where d: "d > 0" "\<And>y. \<bar>y - 0\<bar> < d \<Longrightarrow> \<bar>q y - q 0\<bar> < e" using `e > 0`
  12.471 +        using q(2) \<open>0 \<in> I\<close> \<open>open I\<close> \<open>interior I = I\<close> continuous_on_interior convex_on_continuous by blast
  12.472 +      then obtain d where d: "d > 0" "\<And>y. \<bar>y - 0\<bar> < d \<Longrightarrow> \<bar>q y - q 0\<bar> < e" using \<open>e > 0\<close>
  12.473          by (metis continuous_at_real_range real_norm_def)
  12.474        then have *: "\<bar>q(y)\<bar> > e" if "\<bar>y\<bar> < d" for y
  12.475        proof -
  12.476 @@ -1282,7 +1282,7 @@
  12.477          then show ?thesis unfolding e_def by simp
  12.478        qed
  12.479        have "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} \<le> emeasure M ({x \<in> space M. 1 \<le> ennreal(1/e) * \<bar>q(X x)\<bar>} \<inter> space M)"
  12.480 -        by (rule emeasure_mono, auto simp add: * `e>0` less_imp_le ennreal_mult''[symmetric])
  12.481 +        by (rule emeasure_mono, auto simp add: * \<open>e>0\<close> less_imp_le ennreal_mult''[symmetric])
  12.482        also have "... \<le> (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) * indicator (space M) x \<partial>M)"
  12.483          by (rule nn_integral_Markov_inequality, auto)
  12.484        also have "... = (1/e) * (\<integral>\<^sup>+x. ennreal(\<bar>q(X x)\<bar>) \<partial>M)" by auto
  12.485 @@ -1293,7 +1293,7 @@
  12.486        finally have A: "emeasure M {x \<in> space M. \<bar>X x\<bar> < d} < \<infinity>" by simp
  12.487  
  12.488        have "{x \<in> space M. \<bar>X x\<bar> \<ge> d} = {x \<in> space M. 1 \<le> ennreal(1/d) * \<bar>X x\<bar>} \<inter> space M"
  12.489 -        by (auto simp add: `d>0` ennreal_mult''[symmetric])
  12.490 +        by (auto simp add: \<open>d>0\<close> ennreal_mult''[symmetric])
  12.491        then have "emeasure M {x \<in> space M. \<bar>X x\<bar> \<ge> d} = emeasure M ({x \<in> space M. 1 \<le> ennreal(1/d) * \<bar>X x\<bar>} \<inter> space M)"
  12.492          by auto
  12.493        also have "... \<le> (1/d) * (\<integral>\<^sup>+x. ennreal(\<bar>X x\<bar>) * indicator (space M) x \<partial>M)"
  12.494 @@ -1311,13 +1311,13 @@
  12.495        also have "... \<le> emeasure M {x \<in> space M. \<bar>X x\<bar> < d} + emeasure M {x \<in> space M. \<bar>X x\<bar> \<ge> d}"
  12.496          by (auto intro!: emeasure_subadditive)
  12.497        also have "... < \<infinity>" using A B by auto
  12.498 -      finally show False using `emeasure M (space M) = \<infinity>` by auto
  12.499 +      finally show False using \<open>emeasure M (space M) = \<infinity>\<close> by auto
  12.500      qed
  12.501  
  12.502      define A where "A = Inf ((\<lambda>t. (q 0 - q t) / (0 - t)) ` ({0<..} \<inter> I))"
  12.503      have "q y \<ge> q 0 + A * (y - 0)" if "y \<in> I" for y unfolding A_def apply (rule convex_le_Inf_differential)
  12.504 -      using `0 \<in> I` `y \<in> I` `interior I = I` q(2) by auto
  12.505 -    then have "q y \<ge> A * y" if "y \<in> I" for y using `q 0 = 0` that by auto
  12.506 +      using \<open>0 \<in> I\<close> \<open>y \<in> I\<close> \<open>interior I = I\<close> q(2) by auto
  12.507 +    then have "q y \<ge> A * y" if "y \<in> I" for y using \<open>q 0 = 0\<close> that by auto
  12.508      then have "AE x in M. q (real_cond_exp M F X x) \<ge> A * real_cond_exp M F X x"
  12.509        using real_cond_exp_jensens_inequality(1)[OF X I q] by auto
  12.510      moreover have "AE x in M. q (real_cond_exp M F X x) \<le> real_cond_exp M F (\<lambda>x. q (X x)) x"
    13.1 --- a/src/HOL/Probability/Essential_Supremum.thy	Tue Dec 19 14:51:27 2017 +0100
    13.2 +++ b/src/HOL/Probability/Essential_Supremum.thy	Tue Dec 19 13:58:12 2017 +0100
    13.3 @@ -10,12 +10,12 @@
    13.4  lemma ae_filter_eq_bot_iff: "ae_filter M = bot \<longleftrightarrow> emeasure M (space M) = 0"
    13.5    by (simp add: AE_iff_measurable trivial_limit_def)
    13.6  
    13.7 -section {*The essential supremum*}
    13.8 +section \<open>The essential supremum\<close>
    13.9  
   13.10 -text {*In this paragraph, we define the essential supremum and give its basic properties. The
   13.11 +text \<open>In this paragraph, we define the essential supremum and give its basic properties. The
   13.12  essential supremum of a function is its maximum value if one is allowed to throw away a set
   13.13  of measure $0$. It is convenient to define it to be infinity for non-measurable functions, as
   13.14 -it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.*}
   13.15 +it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.\<close>
   13.16  
   13.17  definition esssup::"'a measure \<Rightarrow> ('a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology, complete_linorder}) \<Rightarrow> 'b"
   13.18    where "esssup M f = (if f \<in> borel_measurable M then Limsup (ae_filter M) f else top)"
   13.19 @@ -56,14 +56,14 @@
   13.20    have *: "{x \<in> space M. f x > z} \<in> null_sets M" if "z > esssup M f" for z
   13.21    proof -
   13.22      have "\<exists>w. w < z \<and> emeasure M {x \<in> space M. f x > w} = 0"
   13.23 -      using `z > esssup M f` f by (auto simp: esssup_eq Inf_less_iff)
   13.24 +      using \<open>z > esssup M f\<close> f by (auto simp: esssup_eq Inf_less_iff)
   13.25      then obtain w where "w < z" "emeasure M {x \<in> space M. f x > w} = 0" by auto
   13.26      then have a: "{x \<in> space M. f x > w} \<in> null_sets M" by auto
   13.27 -    have b: "{x \<in> space M. f x > z} \<subseteq> {x \<in> space M. f x > w}" using `w < z` by auto
   13.28 +    have b: "{x \<in> space M. f x > z} \<subseteq> {x \<in> space M. f x > w}" using \<open>w < z\<close> by auto
   13.29      show ?thesis using null_sets_subset[OF a _ b] by simp
   13.30    qed
   13.31    obtain u::"nat \<Rightarrow> 'b" where u: "\<And>n. u n > esssup M f" "u \<longlonglongrightarrow> esssup M f"
   13.32 -    using approx_from_above_dense_linorder[OF `esssup M f < top`] by auto
   13.33 +    using approx_from_above_dense_linorder[OF \<open>esssup M f < top\<close>] by auto
   13.34    have "{x \<in> space M. f x > esssup M f} = (\<Union>n. {x \<in> space M. f x > u n})"
   13.35      using u apply auto
   13.36      apply (metis (mono_tags, lifting) order_tendsto_iff eventually_mono LIMSEQ_unique)
    14.1 --- a/src/HOL/Probability/Giry_Monad.thy	Tue Dec 19 14:51:27 2017 +0100
    14.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Tue Dec 19 13:58:12 2017 +0100
    14.3 @@ -1746,19 +1746,19 @@
    14.4    shows "bind M f = bind N g"
    14.5  proof cases
    14.6    assume "space N = {}" then show ?thesis
    14.7 -    using `M = N` by (simp add: bind_empty)
    14.8 +    using \<open>M = N\<close> by (simp add: bind_empty)
    14.9  next
   14.10    assume "space N \<noteq> {}"
   14.11 -  show ?thesis unfolding `M = N`
   14.12 +  show ?thesis unfolding \<open>M = N\<close>
   14.13    proof (rule measure_eqI)
   14.14      have *: "sets (N \<bind> f) = sets B"
   14.15 -      using sets_bind[OF sets_kernel[OF f] `space N \<noteq> {}`] by simp
   14.16 +      using sets_bind[OF sets_kernel[OF f] \<open>space N \<noteq> {}\<close>] by simp
   14.17      then show "sets (N \<bind> f) = sets (N \<bind> g)"
   14.18 -      using sets_bind[OF sets_kernel[OF g] `space N \<noteq> {}`] by auto
   14.19 +      using sets_bind[OF sets_kernel[OF g] \<open>space N \<noteq> {}\<close>] by auto
   14.20      fix A assume "A \<in> sets (N \<bind> f)"
   14.21      then have "A \<in> sets B"
   14.22        unfolding * .
   14.23 -    with ae f g `space N \<noteq> {}` show "emeasure (N \<bind> f) A = emeasure (N \<bind> g) A"
   14.24 +    with ae f g \<open>space N \<noteq> {}\<close> show "emeasure (N \<bind> f) A = emeasure (N \<bind> g) A"
   14.25        by (subst (1 2) emeasure_bind[where N=B]) (auto intro!: nn_integral_cong_AE)
   14.26    qed
   14.27  qed
    15.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Tue Dec 19 14:51:27 2017 +0100
    15.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Tue Dec 19 13:58:12 2017 +0100
    15.3 @@ -808,7 +808,7 @@
    15.4    finally show ?thesis .
    15.5  qed
    15.6  
    15.7 -lemma continuous_on_LINT_pmf: -- \<open>This is dominated convergence!?\<close>
    15.8 +lemma continuous_on_LINT_pmf: \<comment> \<open>This is dominated convergence!?\<close>
    15.9    fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> 'b::{banach, second_countable_topology}"
   15.10    assumes f: "\<And>i. i \<in> set_pmf M \<Longrightarrow> continuous_on A (f i)"
   15.11      and bnd: "\<And>a i. a \<in> A \<Longrightarrow> i \<in> set_pmf M \<Longrightarrow> norm (f i a) \<le> B"
    16.1 --- a/src/HOL/Probability/Stopping_Time.thy	Tue Dec 19 14:51:27 2017 +0100
    16.2 +++ b/src/HOL/Probability/Stopping_Time.thy	Tue Dec 19 13:58:12 2017 +0100
    16.3 @@ -1,6 +1,6 @@
    16.4  (* Author: Johannes Hölzl <hoelzl@in.tum.de> *)
    16.5  
    16.6 -section {* Stopping times *}
    16.7 +section \<open>Stopping times\<close>
    16.8  
    16.9  theory Stopping_Time
   16.10    imports "HOL-Analysis.Analysis"
    17.1 --- a/src/HOL/Real.thy	Tue Dec 19 14:51:27 2017 +0100
    17.2 +++ b/src/HOL/Real.thy	Tue Dec 19 13:58:12 2017 +0100
    17.3 @@ -23,7 +23,7 @@
    17.4  
    17.5  subsection \<open>Preliminary lemmas\<close>
    17.6  
    17.7 -text{*Useful in convergence arguments*}
    17.8 +text\<open>Useful in convergence arguments\<close>
    17.9  lemma inverse_of_nat_le:
   17.10    fixes n::nat shows "\<lbrakk>n \<le> m; n\<noteq>0\<rbrakk> \<Longrightarrow> 1 / of_nat m \<le> (1::'a::linordered_field) / of_nat n"
   17.11    by (simp add: frac_le)
    18.1 --- a/src/HOL/Rings.thy	Tue Dec 19 14:51:27 2017 +0100
    18.2 +++ b/src/HOL/Rings.thy	Tue Dec 19 13:58:12 2017 +0100
    18.3 @@ -1273,7 +1273,7 @@
    18.4      and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
    18.5      and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
    18.6      and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
    18.7 -  -- \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
    18.8 +  \<comment> \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
    18.9    
   18.10  class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
   18.11    fixes normalize :: "'a \<Rightarrow> 'a"
    19.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Tue Dec 19 14:51:27 2017 +0100
    19.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Tue Dec 19 13:58:12 2017 +0100
    19.3 @@ -380,7 +380,7 @@
    19.4    using assms by (metis mult_le_0_iff)
    19.5  
    19.6  
    19.7 -subsection {* Linear arithmetic for natural numbers *}
    19.8 +subsection \<open>Linear arithmetic for natural numbers\<close>
    19.9  
   19.10  declare [[smt_nat_as_int]]
   19.11  
    20.1 --- a/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Dec 19 14:51:27 2017 +0100
    20.2 +++ b/src/HOL/SMT_Examples/SMT_Tests.thy	Tue Dec 19 13:58:12 2017 +0100
    20.3 @@ -222,7 +222,7 @@
    20.4    by smt+
    20.5  
    20.6  
    20.7 -section {* Natural numbers *}
    20.8 +section \<open>Natural numbers\<close>
    20.9  
   20.10  declare [[smt_nat_as_int]]
   20.11  
    21.1 --- a/src/HOL/Topological_Spaces.thy	Tue Dec 19 14:51:27 2017 +0100
    21.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Dec 19 13:58:12 2017 +0100
    21.3 @@ -1486,10 +1486,10 @@
    21.4      by (metis first_countable_topology_class.countable_basis)
    21.5    define u where "u = (\<lambda>n. SOME z. z \<in> A n \<and> z > x)"
    21.6    have "\<exists>z. z \<in> U \<and> x < z" if "x \<in> U" "open U" for U
    21.7 -    using open_right[OF `open U` `x \<in> U` `x < y`]
    21.8 +    using open_right[OF \<open>open U\<close> \<open>x \<in> U\<close> \<open>x < y\<close>]
    21.9      by (meson atLeastLessThan_iff dense less_imp_le subset_eq)
   21.10    then have *: "u n \<in> A n \<and> x < u n" for n
   21.11 -    using `x \<in> A n` `open (A n)` unfolding u_def by (metis (no_types, lifting) someI_ex)
   21.12 +    using \<open>x \<in> A n\<close> \<open>open (A n)\<close> unfolding u_def by (metis (no_types, lifting) someI_ex)
   21.13    then have "u \<longlonglongrightarrow> x" using A(3) by simp
   21.14    then show ?thesis using * by auto
   21.15  qed
   21.16 @@ -1504,10 +1504,10 @@
   21.17      by (metis first_countable_topology_class.countable_basis)
   21.18    define u where "u = (\<lambda>n. SOME z. z \<in> A n \<and> z < x)"
   21.19    have "\<exists>z. z \<in> U \<and> z < x" if "x \<in> U" "open U" for U
   21.20 -    using open_left[OF `open U` `x \<in> U` `x > y`]
   21.21 +    using open_left[OF \<open>open U\<close> \<open>x \<in> U\<close> \<open>x > y\<close>]
   21.22      by (meson dense greaterThanAtMost_iff less_imp_le subset_eq)
   21.23    then have *: "u n \<in> A n \<and> u n < x" for n
   21.24 -    using `x \<in> A n` `open (A n)` unfolding u_def by (metis (no_types, lifting) someI_ex)
   21.25 +    using \<open>x \<in> A n\<close> \<open>open (A n)\<close> unfolding u_def by (metis (no_types, lifting) someI_ex)
   21.26    then have "u \<longlonglongrightarrow> x" using A(3) by simp
   21.27    then show ?thesis using * by auto
   21.28  qed
   21.29 @@ -3478,7 +3478,7 @@
   21.30      by (auto simp add: separation_t2)
   21.31    define T where "T = U \<times> V"
   21.32    have "open T" using * open_Times T_def by auto
   21.33 -  moreover have "t \<in> T" unfolding T_def using `t = (x,y)` * by auto
   21.34 +  moreover have "t \<in> T" unfolding T_def using \<open>t = (x,y)\<close> * by auto
   21.35    moreover have "T \<subseteq> {(x, y) | x y. x \<noteq> y}" unfolding T_def using * by auto
   21.36    ultimately show "\<exists>T. open T \<and> t \<in> T \<and> T \<subseteq> {(x, y) | x y. x \<noteq> y}" by auto
   21.37  qed
   21.38 @@ -3501,18 +3501,18 @@
   21.39      then obtain z where z: "y < z \<and> z < x" by blast
   21.40      define T where "T = {z<..} \<times> {..<z}"
   21.41      have "open T" unfolding T_def by (simp add: open_Times)
   21.42 -    moreover have "t \<in> T" using T_def z `t = (x,y)` by auto
   21.43 +    moreover have "t \<in> T" using T_def z \<open>t = (x,y)\<close> by auto
   21.44      moreover have "T \<subseteq> {(x, y) | x y. y < x}" unfolding T_def by auto
   21.45      ultimately show ?thesis by auto
   21.46    next
   21.47      assume "\<not>(\<exists>z. y < z \<and> z < x)"
   21.48      then have *: "{x ..} = {y<..}" "{..< x} = {..y}"
   21.49 -      using `x > y` apply auto using leI by blast
   21.50 +      using \<open>x > y\<close> apply auto using leI by blast
   21.51      define T where "T = {x ..} \<times> {.. y}"
   21.52      then have "T = {y<..} \<times> {..< x}" using * by simp
   21.53      then have "open T" unfolding T_def by (simp add: open_Times)
   21.54 -    moreover have "t \<in> T" using T_def `t = (x,y)` by auto
   21.55 -    moreover have "T \<subseteq> {(x, y) | x y. y < x}" unfolding T_def using `x > y` by auto
   21.56 +    moreover have "t \<in> T" using T_def \<open>t = (x,y)\<close> by auto
   21.57 +    moreover have "T \<subseteq> {(x, y) | x y. y < x}" unfolding T_def using \<open>x > y\<close> by auto
   21.58      ultimately show ?thesis by auto
   21.59    qed
   21.60  qed
   21.61 @@ -3535,18 +3535,18 @@
   21.62      then obtain z where z: "y > z \<and> z > x" by blast
   21.63      define T where "T = {..<z} \<times> {z<..}"
   21.64      have "open T" unfolding T_def by (simp add: open_Times)
   21.65 -    moreover have "t \<in> T" using T_def z `t = (x,y)` by auto
   21.66 +    moreover have "t \<in> T" using T_def z \<open>t = (x,y)\<close> by auto
   21.67      moreover have "T \<subseteq> {(x, y) |x y. y > x}" unfolding T_def by auto
   21.68      ultimately show ?thesis by auto
   21.69    next
   21.70      assume "\<not>(\<exists>z. y > z \<and> z > x)"
   21.71      then have *: "{..x} = {..<y}" "{x<..} = {y..}"
   21.72 -      using `x < y` apply auto using leI by blast
   21.73 +      using \<open>x < y\<close> apply auto using leI by blast
   21.74      define T where "T = {..x} \<times> {y..}"
   21.75      then have "T = {..<y} \<times> {x<..}" using * by simp
   21.76      then have "open T" unfolding T_def by (simp add: open_Times)
   21.77 -    moreover have "t \<in> T" using T_def `t = (x,y)` by auto
   21.78 -    moreover have "T \<subseteq> {(x, y) |x y. y > x}" unfolding T_def using `x < y` by auto
   21.79 +    moreover have "t \<in> T" using T_def \<open>t = (x,y)\<close> by auto
   21.80 +    moreover have "T \<subseteq> {(x, y) |x y. y > x}" unfolding T_def using \<open>x < y\<close> by auto
   21.81      ultimately show ?thesis by auto
   21.82    qed
   21.83  qed
    22.1 --- a/src/HOL/ex/Perm_Fragments.thy	Tue Dec 19 14:51:27 2017 +0100
    22.2 +++ b/src/HOL/ex/Perm_Fragments.thy	Tue Dec 19 13:58:12 2017 +0100
    22.3 @@ -97,7 +97,7 @@
    22.4  lemma orbit_cycle_elem:
    22.5    assumes "distinct as" and "a \<in> set as"
    22.6    shows "orbit \<langle>as\<rangle> a = set as"
    22.7 -  oops -- \<open>(we need rotation here\<close>
    22.8 +  oops \<comment> \<open>(we need rotation here\<close>
    22.9  
   22.10  lemma order_cycle_elem:
   22.11    assumes "distinct as" and "a \<in> set as"