author wenzelm Tue Dec 19 13:58:12 2017 +0100 (17 months ago) changeset 67226 ec32cdaab97b parent 67225 cb34f5f49a08 child 67227 6f6b26557ea9 child 67228 7c7b76695c90
isabelle update_cartouches -c -t;
 src/HOL/Algebra/Complete_Lattice.thy file | annotate | diff | revisions src/HOL/Algebra/Lattice.thy file | annotate | diff | revisions src/HOL/Algebra/Multiplicative_Group.thy file | annotate | diff | revisions src/HOL/Analysis/Bounded_Linear_Function.thy file | annotate | diff | revisions src/HOL/Auth/Yahalom.thy file | annotate | diff | revisions src/HOL/Auth/Yahalom2.thy file | annotate | diff | revisions src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy file | annotate | diff | revisions src/HOL/Divides.thy file | annotate | diff | revisions src/HOL/Fun.thy file | annotate | diff | revisions src/HOL/Power.thy file | annotate | diff | revisions src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy file | annotate | diff | revisions src/HOL/Probability/Conditional_Expectation.thy file | annotate | diff | revisions src/HOL/Probability/Essential_Supremum.thy file | annotate | diff | revisions src/HOL/Probability/Giry_Monad.thy file | annotate | diff | revisions src/HOL/Probability/Probability_Mass_Function.thy file | annotate | diff | revisions src/HOL/Probability/Stopping_Time.thy file | annotate | diff | revisions src/HOL/Real.thy file | annotate | diff | revisions src/HOL/Rings.thy file | annotate | diff | revisions src/HOL/SMT_Examples/SMT_Examples.thy file | annotate | diff | revisions src/HOL/SMT_Examples/SMT_Tests.thy file | annotate | diff | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | revisions src/HOL/ex/Perm_Fragments.thy file | annotate | diff | revisions
     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.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.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.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.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.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"

    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"