src/HOL/Analysis/Borel_Space.thy
 changeset 64911 f0e07600de47 parent 64320 ba194424b895 child 66164 2d79288b042c
```     1.1 --- a/src/HOL/Analysis/Borel_Space.thy	Tue Jan 17 11:26:21 2017 +0100
1.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Tue Jan 17 13:59:10 2017 +0100
1.3 @@ -2126,7 +2126,7 @@
1.4    shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> borel_measurable M"
1.5  unfolding powr_def by auto
1.6
1.7 -text {* The next one is a variation around \verb+measurable_restrict_space+.*}
1.8 +text \<open>The next one is a variation around \verb+measurable_restrict_space+.\<close>
1.9
1.10  lemma measurable_restrict_space3:
1.11    assumes "f \<in> measurable M N" and
1.12 @@ -2138,7 +2138,7 @@
1.13        measurable_restrict_space2[of f, of "restrict_space M A", of B, of N] assms(2) space_restrict_space)
1.14  qed
1.15
1.16 -text {* The next one is a variation around \verb+measurable_piecewise_restrict+.*}
1.17 +text \<open>The next one is a variation around \verb+measurable_piecewise_restrict+.\<close>
1.18
1.19  lemma measurable_piecewise_restrict2:
1.20    assumes [measurable]: "\<And>n. A n \<in> sets M"
1.21 @@ -2162,8 +2162,8 @@
1.22    fix x assume "x \<in> space M"
1.23    then obtain n where "x \<in> A n" using assms(2) by blast
1.24    obtain h where [measurable]: "h \<in> measurable M N" and "\<forall>x \<in> A n. f x = h x" using assms(3) by blast
1.25 -  then have "f x = h x" using `x \<in> A n` by blast
1.26 -  moreover have "h x \<in> space N" by (metis measurable_space `x \<in> space M` `h \<in> measurable M N`)
1.27 +  then have "f x = h x" using \<open>x \<in> A n\<close> by blast
1.28 +  moreover have "h x \<in> space N" by (metis measurable_space \<open>x \<in> space M\<close> \<open>h \<in> measurable M N\<close>)
1.29    ultimately show "f x \<in> space N" by simp
1.30  qed
1.31
```