# HG changeset patch
# User nipkow
# Date 1548424780 -3600
# Node ID 8b47c021666e09cd9c3350939c72fd925597fac6
# Parent  c558fef629157c2de8f3b47e3367f4a59988b46a
tuned

diff -r c558fef62915 -r 8b47c021666e src/HOL/Analysis/Binary_Product_Measure.thy
--- a/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Jan 25 13:19:16 2019 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Fri Jan 25 14:59:40 2019 +0100
@@ -104,13 +104,13 @@
   shows "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2)"
   using measurable_Pair[OF assms] by simp
 
-lemma (*FIX ME needs a name *)
+lemma
   assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^sub>M P)"
   shows measurable_fst': "(\<lambda>x. fst (f x)) \<in> measurable M N"
     and measurable_snd': "(\<lambda>x. snd (f x)) \<in> measurable M P"
   by simp_all
 
-lemma (*FIX ME needs a name *)
+lemma
   assumes f[measurable]: "f \<in> measurable M N"
   shows measurable_fst'': "(\<lambda>x. f (fst x)) \<in> measurable (M \<Otimes>\<^sub>M P) N"
     and measurable_snd'': "(\<lambda>x. f (snd x)) \<in> measurable (P \<Otimes>\<^sub>M M) N"
diff -r c558fef62915 -r 8b47c021666e src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Fri Jan 25 13:19:16 2019 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Fri Jan 25 14:59:40 2019 +0100
@@ -1464,7 +1464,7 @@
   using integral_discrete_difference[of X M f g, OF assms]
   by (metis has_bochner_integral_iff)
 
-lemma (*FIX ME needs name *)
+lemma
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}" and w :: "'a \<Rightarrow> real"
   assumes "f \<in> borel_measurable M" "\<And>i. s i \<in> borel_measurable M" "integrable M w"
   assumes lim: "AE x in M. (\<lambda>i. s i x) \<longlonglongrightarrow> f x"
@@ -1697,7 +1697,7 @@
     by (simp_all add: * assms integral_nonneg_AE)
 qed
 
-lemma (* FIX ME needs name*)
+lemma
   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> 'a :: {banach, second_countable_topology}"
   assumes integrable[measurable]: "\<And>i. integrable M (f i)"
   and summable: "AE x in M. summable (\<lambda>i. norm (f i x))"
@@ -2327,7 +2327,7 @@
   qed
 qed (simp add: f g integrable_density)
 
-lemma (*FIX ME needs name *)
+lemma
   fixes g :: "'a \<Rightarrow> real"
   assumes "f \<in> borel_measurable M" "AE x in M. 0 \<le> f x" "g \<in> borel_measurable M"
   shows integral_real_density: "integral\<^sup>L (density M f) g = (\<integral> x. f x * g x \<partial>M)"
@@ -2630,7 +2630,7 @@
     by (auto simp: real_integrable_def real_lebesgue_integral_def u)
 qed
 
-lemma (*FIX ME needs name *)
+lemma
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> real"
   assumes f: "\<And>i. integrable M (f i)" and mono: "AE x in M. mono (\<lambda>n. f n x)"
   and lim: "AE x in M. (\<lambda>i. f i x) \<longlonglongrightarrow> u x"
@@ -2810,7 +2810,7 @@
   qed auto
 qed
 
-lemma (*FIX ME needs name *)
+lemma
   fixes f :: "real \<Rightarrow> real"
   assumes M: "sets M = sets borel"
   assumes nonneg: "AE x in M. 0 \<le> f x"
@@ -3154,7 +3154,7 @@
   qed
 qed
 
-lemma (in pair_sigma_finite) (* FIX ME needs name *)
+lemma (in pair_sigma_finite)
   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
   assumes f: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
   shows AE_integrable_fst: "AE x in M1. integrable M2 (\<lambda>y. f x y)" (is "?AE")
@@ -3162,7 +3162,7 @@
     and integral_fst: "(\<integral>x. (\<integral>y. f x y \<partial>M2) \<partial>M1) = integral\<^sup>L (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). f x y)" (is "?EQ")
   using AE_integrable_fst'[OF f] integrable_fst'[OF f] integral_fst'[OF f] by auto
 
-lemma (in pair_sigma_finite) (* FIX ME needs name *)
+lemma (in pair_sigma_finite)
   fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _::{banach, second_countable_topology}"
   assumes f[measurable]: "integrable (M1 \<Otimes>\<^sub>M M2) (case_prod f)"
   shows AE_integrable_snd: "AE y in M2. integrable M1 (\<lambda>x. f x y)" (is "?AE")
diff -r c558fef62915 -r 8b47c021666e src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Fri Jan 25 13:19:16 2019 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy	Fri Jan 25 14:59:40 2019 +0100
@@ -797,7 +797,7 @@
   finally show ?thesis .
 qed
 
-lemma (* FIX ME needs name *)
+lemma
   fixes f :: "'a \<Rightarrow> 'b::{second_countable_topology, linorder_topology}"
   assumes f[measurable]: "f \<in> borel_measurable M"
   assumes g[measurable]: "g \<in> borel_measurable M"
@@ -929,7 +929,7 @@
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (\<lambda>x. inf (g x) (f x) :: 'b::{lattice, second_countable_topology, linorder_topology}) \<in> borel_measurable M"
   unfolding inf_min by measurable
 
-lemma [measurable (raw)]: (*FIXME needs name *)
+lemma [measurable (raw)]:
   fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::{complete_linorder, second_countable_topology, linorder_topology}"
   assumes "\<And>i. f i \<in> borel_measurable M"
   shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
@@ -1023,7 +1023,7 @@
   unfolding box_oc box_co
   by (auto intro: borel_open borel_closed)
 
-lemma (*FIX ME this has no name *)
+lemma
   fixes i :: "'a::{second_countable_topology, real_inner}"
   shows hafspace_less_borel: "{x. a < x \<bullet> i} \<in> sets borel"
     and hafspace_greater_borel: "{x. x \<bullet> i < a} \<in> sets borel"
@@ -1551,7 +1551,7 @@
   with f H show ?thesis by simp
 qed
 
-lemma (*FIX ME needs a name *)
+lemma
   fixes f :: "'a \<Rightarrow> ereal" assumes f[measurable]: "f \<in> borel_measurable M"
   shows borel_measurable_ereal_abs[measurable(raw)]: "(\<lambda>x. \<bar>f x\<bar>) \<in> borel_measurable M"
     and borel_measurable_ereal_inverse[measurable(raw)]: "(\<lambda>x. inverse (f x) :: ereal) \<in> borel_measurable M"
diff -r c558fef62915 -r 8b47c021666e src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Fri Jan 25 13:19:16 2019 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Fri Jan 25 14:59:40 2019 +0100
@@ -963,12 +963,12 @@
   then show "f ` S \<in> lmeasurable" ?M by blast+
 qed
 
-lemma (*FIXME needs name? *)
+lemma m_diff_image_weak:
  fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
   assumes S: "S \<in> lmeasurable"
     and deriv: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
     and int: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S"
-  shows m_diff_image_weak: "f ` S \<in> lmeasurable \<and> measure lebesgue (f ` S) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"
+  shows "f ` S \<in> lmeasurable \<and> measure lebesgue (f ` S) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"
 proof -
   let ?\<mu> = "measure lebesgue"
   have aint_S: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) absolutely_integrable_on S"
@@ -1161,7 +1161,7 @@
 qed
 
 
-theorem(* FIXME needs name? *)
+theorem
  fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
   assumes S: "S \<in> sets lebesgue"
     and deriv: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
diff -r c558fef62915 -r 8b47c021666e src/HOL/Analysis/Finite_Product_Measure.thy
--- a/src/HOL/Analysis/Finite_Product_Measure.thy	Fri Jan 25 13:19:16 2019 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy	Fri Jan 25 14:59:40 2019 +0100
@@ -397,7 +397,7 @@
   apply (auto intro!: arg_cong2[where f=sigma_sets])
   done
 
-lemma (*FIX ME needs name *)
+lemma
   shows space_PiM_empty: "space (Pi\<^sub>M {} M) = {\<lambda>k. undefined}"
     and sets_PiM_empty: "sets (Pi\<^sub>M {} M) = { {}, {\<lambda>k. undefined} }"
   by (simp_all add: space_PiM sets_PiM_single image_constant sigma_sets_empty_eq)
diff -r c558fef62915 -r 8b47c021666e src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Fri Jan 25 13:19:16 2019 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy	Fri Jan 25 14:59:40 2019 +0100
@@ -278,7 +278,7 @@
   qed
 qed
 
-proposition (*FIXME needs name *)
+proposition
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and 0: "0 \<in> rel_interior S"
       and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment 0 x \<subseteq> rel_interior S"
@@ -540,7 +540,7 @@
     done
 qed
 
-corollary (* FIXME needs name *)
+corollary
   fixes S :: "'a::euclidean_space set"
   assumes "compact S" and a: "a \<in> rel_interior S"
       and star: "\<And>x. x \<in> S \<Longrightarrow> open_segment a x \<subseteq> rel_interior S"
diff -r c558fef62915 -r 8b47c021666e src/HOL/Analysis/Poly_Roots.thy
--- a/src/HOL/Analysis/Poly_Roots.thy	Fri Jan 25 13:19:16 2019 +0100
+++ b/src/HOL/Analysis/Poly_Roots.thy	Fri Jan 25 14:59:40 2019 +0100
@@ -182,7 +182,7 @@
    qed simp
 qed simp
 
-corollary (*FIX ME needs name *)
+corollary
   fixes c :: "nat \<Rightarrow> 'a::{comm_ring,real_normed_div_algebra}"
   assumes "\<exists>k. k \<le> n \<and> c k \<noteq> 0"
     shows polyfun_rootbound_finite: "finite {z. (\<Sum>i\<le>n. c i * z^i) = 0}"
diff -r c558fef62915 -r 8b47c021666e src/HOL/Analysis/Radon_Nikodym.thy
--- a/src/HOL/Analysis/Radon_Nikodym.thy	Fri Jan 25 13:19:16 2019 +0100
+++ b/src/HOL/Analysis/Radon_Nikodym.thy	Fri Jan 25 14:59:40 2019 +0100
@@ -1022,7 +1022,7 @@
     by simp
 qed
 
-lemma (in sigma_finite_measure) (* FIXME needs name*)
+lemma (in sigma_finite_measure)
   assumes N: "sigma_finite_measure N" and ac: "absolutely_continuous M N" "sets N = sets M"
     and f: "f \<in> borel_measurable M"
   shows RN_deriv_integrable: "integrable N f \<longleftrightarrow>
diff -r c558fef62915 -r 8b47c021666e src/HOL/Analysis/Regularity.thy
--- a/src/HOL/Analysis/Regularity.thy	Fri Jan 25 13:19:16 2019 +0100
+++ b/src/HOL/Analysis/Regularity.thy	Fri Jan 25 14:59:40 2019 +0100
@@ -9,7 +9,7 @@
 imports Measure_Space Borel_Space
 begin
 
-theorem (*FIX needs name *)
+theorem
   fixes M::"'a::{second_countable_topology, complete_space} measure"
   assumes sb: "sets M = sets borel"
   assumes "emeasure M (space M) \<noteq> \<infinity>"