--- 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"
--- 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")
--- 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"
--- 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)"
--- 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)
--- 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"
--- 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}"
--- 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>
--- 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>"