--- a/src/HOL/Analysis/Sigma_Algebra.thy Mon Jul 09 21:55:40 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Tue Jul 10 09:38:35 2018 +0200
@@ -146,13 +146,13 @@
"a \<in> M \<Longrightarrow> \<Omega> - a \<in> M"
by auto
-lemma%important algebra_iff_Un:
+proposition algebra_iff_Un:
"algebra \<Omega> M \<longleftrightarrow>
M \<subseteq> Pow \<Omega> \<and>
{} \<in> M \<and>
(\<forall>a \<in> M. \<Omega> - a \<in> M) \<and>
(\<forall>a \<in> M. \<forall> b \<in> M. a \<union> b \<in> M)" (is "_ \<longleftrightarrow> ?Un")
-proof%unimportant
+proof
assume "algebra \<Omega> M"
then interpret algebra \<Omega> M .
show ?Un using sets_into_space by auto
@@ -173,12 +173,12 @@
show "algebra \<Omega> M" proof qed fact
qed
-lemma%important algebra_iff_Int:
+proposition algebra_iff_Int:
"algebra \<Omega> M \<longleftrightarrow>
M \<subseteq> Pow \<Omega> & {} \<in> M &
(\<forall>a \<in> M. \<Omega> - a \<in> M) &
(\<forall>a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)" (is "_ \<longleftrightarrow> ?Int")
-proof%unimportant
+proof
assume "algebra \<Omega> M"
then interpret algebra \<Omega> M .
show ?Int using sets_into_space by auto
@@ -1433,7 +1433,7 @@
text%important \<open>The reason to introduce Dynkin-systems is the following induction rules for $\sigma$-algebras
generated by a generator closed under intersection.\<close>
-lemma%important sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
+proposition sigma_sets_induct_disjoint[consumes 3, case_names basic empty compl union]:
assumes "Int_stable G"
and closed: "G \<subseteq> Pow \<Omega>"
and A: "A \<in> sigma_sets \<Omega> G"
@@ -1442,7 +1442,7 @@
and compl: "\<And>A. A \<in> sigma_sets \<Omega> G \<Longrightarrow> P A \<Longrightarrow> P (\<Omega> - A)"
and union: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> sigma_sets \<Omega> G \<Longrightarrow> (\<And>i. P (A i)) \<Longrightarrow> P (\<Union>i::nat. A i)"
shows "P A"
-proof%unimportant -
+proof -
let ?D = "{ A \<in> sigma_sets \<Omega> G. P A }"
interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
using closed by (rule sigma_algebra_sigma_sets)
@@ -1633,12 +1633,12 @@
subsubsection \<open>Constructing simple @{typ "'a measure"}\<close>
-lemma%important emeasure_measure_of:
+proposition emeasure_measure_of:
assumes M: "M = measure_of \<Omega> A \<mu>"
assumes ms: "A \<subseteq> Pow \<Omega>" "positive (sets M) \<mu>" "countably_additive (sets M) \<mu>"
assumes X: "X \<in> sets M"
shows "emeasure M X = \<mu> X"
-proof%unimportant -
+proof -
interpret sigma_algebra \<Omega> "sigma_sets \<Omega> A" by (rule sigma_algebra_sigma_sets) fact
have "measure_space \<Omega> (sigma_sets \<Omega> A) \<mu>"
using ms M by (simp add: measure_space_def sigma_algebra_sigma_sets)