# HG changeset patch
# User Andreas Lochbihler
# Date 1546363999 -3600
# Node ID 2d88bf80c84f3ec47106332b04f4ea5412d3b8ae
# Parent  a59f7d07bf1748638c22533801b27430788c489d# Parent  de09a7261120557937026a4b401c4834264afd1c
merged

diff -r de09a7261120 -r 2d88bf80c84f NEWS
--- a/NEWS	Tue Jan 01 17:04:53 2019 +0100
+++ b/NEWS	Tue Jan 01 18:33:19 2019 +0100
@@ -84,7 +84,8 @@
 INCOMPATIBILITY.
 
 * Strong congruence rules (with =simp=> in the premises) for constant f
-are now uniformly called f_cong_strong. 
+are now uniformly called f_cong_simp, in accordance with congruence
+rules produced for mappers by the datatype package. INCOMPATIBILITY.
 
 * Sledgehammer: The URL for SystemOnTPTP, which is used by remote
 provers, has been updated.
diff -r de09a7261120 -r 2d88bf80c84f src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -189,7 +189,9 @@
   \<close>}
 
   A @{syntax_def system_name} is like @{syntax name}, but it excludes
-  white-space characters and needs to conform to file-name notation.
+  white-space characters and needs to conform to file-name notation. Name
+  components that are special on Windows (e.g.\ \<^verbatim>\<open>CON\<close>, \<^verbatim>\<open>PRN\<close>, \<^verbatim>\<open>AUX\<close>) are
+  excluded on all platforms.
 \<close>
 
 
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -524,7 +524,7 @@
   assumes "M = N" "\<And>x. x \<in> space N \<Longrightarrow> f x = g x" "x = y"
   shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral N g y"
   unfolding has_bochner_integral.simps assms(1,3)
-  using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong)
+  using assms(2) by (simp cong: measurable_cong_simp nn_integral_cong_simp)
 
 lemma%unimportant has_bochner_integral_cong_AE:
   "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow>
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Analysis/Caratheodory.thy
--- a/src/HOL/Analysis/Caratheodory.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Analysis/Caratheodory.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -737,7 +737,7 @@
           using f C Ai unfolding bij_betw_def by auto
         then have "\<Union>range f = A i"
           using f C Ai unfolding bij_betw_def
-            by (auto simp add: f_def cong del: SUP_cong_strong)
+            by (auto simp add: f_def cong del: SUP_cong_simp)
         moreover
         { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
             using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -2193,7 +2193,7 @@
   using assms(2-3) vector_derivative_works
   by auto
 
-subsection\<open>The notion of being field differentiable\<close>
+subsection \<open>Field differentiability\<close>
 
 definition%important field_differentiable :: "['a \<Rightarrow> 'a::real_normed_field, 'a filter] \<Rightarrow> bool"
            (infixr "(field'_differentiable)" 50)
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Analysis/Elementary_Topology.thy
--- a/src/HOL/Analysis/Elementary_Topology.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -687,7 +687,8 @@
 
 subsection \<open>Interior of a Set\<close>
 
-definition%important "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
+definition%important interior :: "('a::topological_space) set \<Rightarrow> 'a set" where
+"interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
 
 lemma interiorI [intro?]:
   assumes "open T" and "x \<in> T" and "T \<subseteq> S"
@@ -851,7 +852,8 @@
 
 subsection \<open>Closure of a Set\<close>
 
-definition%important "closure S = S \<union> {x | x. x islimpt S}"
+definition%important closure :: "('a::topological_space) set \<Rightarrow> 'a set" where
+"closure S = S \<union> {x . x islimpt S}"
 
 lemma interior_closure: "interior S = - (closure (- S))"
   by (auto simp: interior_def closure_def islimpt_def)
@@ -980,7 +982,8 @@
 
 subsection \<open>Frontier (also known as boundary)\<close>
 
-definition%important "frontier S = closure S - interior S"
+definition%important frontier :: "('a::topological_space) set \<Rightarrow> 'a set" where
+"frontier S = closure S - interior S"
 
 lemma frontier_closed [iff]: "closed (frontier S)"
   by (simp add: frontier_def closed_Diff)
@@ -1630,8 +1633,10 @@
   with \<open>U \<inter> \<Inter>A = {}\<close> show False by auto
 qed
 
-definition%important "countably_compact U \<longleftrightarrow>
-    (\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))"
+definition%important countably_compact :: "('a::topological_space) set \<Rightarrow> bool" where
+"countably_compact U \<longleftrightarrow>
+  (\<forall>A. countable A \<longrightarrow> (\<forall>a\<in>A. open a) \<longrightarrow> U \<subseteq> \<Union>A
+     \<longrightarrow> (\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T))"
 
 lemma countably_compactE:
   assumes "countably_compact s" and "\<forall>t\<in>C. open t" and "s \<subseteq> \<Union>C" "countable C"
@@ -1698,9 +1703,10 @@
 
 subsubsection\<open>Sequential compactness\<close>
 
-definition%important seq_compact :: "'a::topological_space set \<Rightarrow> bool"
-  where "seq_compact S \<longleftrightarrow>
-    (\<forall>f. (\<forall>n. f n \<in> S) \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
+definition%important seq_compact :: "'a::topological_space set \<Rightarrow> bool" where
+"seq_compact S \<longleftrightarrow>
+  (\<forall>f. (\<forall>n. f n \<in> S)
+    \<longrightarrow> (\<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially))"
 
 lemma seq_compactI:
   assumes "\<And>f. \<forall>n. f n \<in> S \<Longrightarrow> \<exists>l\<in>S. \<exists>r::nat\<Rightarrow>nat. strict_mono r \<and> ((f \<circ> r) \<longlongrightarrow> l) sequentially"
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Analysis/L2_Norm.thy
--- a/src/HOL/Analysis/L2_Norm.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -14,7 +14,7 @@
   "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
   unfolding L2_set_def by simp
 
-lemma L2_set_cong_strong:
+lemma L2_set_cong_simp:
   "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
   unfolding L2_set_def simp_implies_def by simp
 
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -407,7 +407,7 @@
 lemma measurable_lebesgue_cong:
   assumes "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
   shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
-  by (metis (mono_tags, lifting) IntD1 assms measurable_cong_strong space_restrict_space)
+  by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space)
 
 text%unimportant \<open>Measurability of continuous functions\<close>
 
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -1143,7 +1143,7 @@
   "(\<And>x. x \<in> space M \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in M. Q x)"
   by auto
 
-lemma AE_cong_strong: "M = N \<Longrightarrow> (\<And>x. x \<in> space N =simp=> P x = Q x) \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in N. Q x)"
+lemma AE_cong_simp: "M = N \<Longrightarrow> (\<And>x. x \<in> space N =simp=> P x = Q x) \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in N. Q x)"
   by (auto simp: simp_implies_def)
 
 lemma AE_all_countable:
@@ -1388,7 +1388,8 @@
 subsection \<open>Measure space induced by distribution of @{const measurable}-functions\<close>
 
 definition%important distr :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure" where
-  "distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
+"distr M N f =
+  measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
 
 lemma
   shows sets_distr[simp, measurable_cong]: "sets (distr M N f) = sets N"
@@ -1708,9 +1709,8 @@
 
 subsection \<open>Set of measurable sets with finite measure\<close>
 
-definition%important fmeasurable :: "'a measure \<Rightarrow> 'a set set"
-where
-  "fmeasurable M = {A\<in>sets M. emeasure M A < \<infinity>}"
+definition%important fmeasurable :: "'a measure \<Rightarrow> 'a set set" where
+"fmeasurable M = {A\<in>sets M. emeasure M A < \<infinity>}"
 
 lemma fmeasurableD[dest, measurable_dest]: "A \<in> fmeasurable M \<Longrightarrow> A \<in> sets M"
   by (auto simp: fmeasurable_def)
@@ -2589,7 +2589,7 @@
       using E \<Omega> by (subst (1 2) emeasure_restrict_space) (auto simp: sets_eq sets_eq[THEN sets_eq_imp_space_eq])
   next
     show "range (from_nat_into A) \<subseteq> E" "(\<Union>i. from_nat_into A i) = \<Omega>"
-      using A by (auto cong del: SUP_cong_strong)
+      using A by (auto cong del: SUP_cong_simp)
   next
     fix i
     have "emeasure (restrict_space M \<Omega>) (from_nat_into A i) = emeasure M (from_nat_into A i)"
@@ -2605,7 +2605,8 @@
 
 subsection%unimportant \<open>Null measure\<close>
 
-definition "null_measure M = sigma (space M) (sets M)"
+definition null_measure :: "'a measure \<Rightarrow> 'a measure" where
+"null_measure M = sigma (space M) (sets M)"
 
 lemma space_null_measure[simp]: "space (null_measure M) = space M"
   by (simp add: null_measure_def)
@@ -2626,9 +2627,8 @@
 
 subsection \<open>Scaling a measure\<close>
 
-definition%important scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
-where
-  "scale_measure r M = measure_of (space M) (sets M) (\<lambda>A. r * emeasure M A)"
+definition%important scale_measure :: "ennreal \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where
+"scale_measure r M = measure_of (space M) (sets M) (\<lambda>A. r * emeasure M A)"
 
 lemma space_scale_measure: "space (scale_measure r M) = space M"
   by (simp add: scale_measure_def)
@@ -2874,9 +2874,10 @@
     by (cases "X \<in> sets M") (auto simp: emeasure_notin_sets)
   done
 
-definition%important sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
-where
-  "sup_measure' A B = measure_of (space A) (sets A) (\<lambda>X. SUP Y\<in>sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
+definition%important sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where
+"sup_measure' A B =
+  measure_of (space A) (sets A)
+    (\<lambda>X. SUP Y\<in>sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
 
 lemma assumes [simp]: "sets B = sets A"
   shows space_sup_measure'[simp]: "space (sup_measure' A B) = space A"
@@ -3002,10 +3003,11 @@
   qed
 qed simp_all
 
-definition%important sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a"
-where
-  "sup_lexord A B k s c =
-    (if k A = k B then c else if \<not> k A \<le> k B \<and> \<not> k B \<le> k A then s else if k B \<le> k A then A else B)"
+definition%important sup_lexord :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b::order) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
+"sup_lexord A B k s c =
+  (if k A = k B then c else
+   if \<not> k A \<le> k B \<and> \<not> k B \<le> k A then s else
+   if k B \<le> k A then A else B)"
 
 lemma sup_lexord:
   "(k A < k B \<Longrightarrow> P B) \<Longrightarrow> (k B < k A \<Longrightarrow> P A) \<Longrightarrow> (k A = k B \<Longrightarrow> P c) \<Longrightarrow>
@@ -3031,8 +3033,7 @@
 instantiation measure :: (type) semilattice_sup
 begin
 
-definition%important sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
-where
+definition%important sup_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where
   "sup_measure A B =
     sup_lexord A B space (sigma (space A \<union> space B) {})
       (sup_lexord A B sets (sigma (space A) (sets A \<union> sets B)) (sup_measure' A B))"
@@ -3135,9 +3136,12 @@
 lemma UN_space_closed: "\<Union>(sets ` S) \<subseteq> Pow (\<Union>(space ` S))"
   using sets.space_closed by auto
 
-definition Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
+definition%important
+  Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
 where
-  "Sup_lexord k c s A = (let U = (SUP a\<in>A. k a) in if \<exists>a\<in>A. k a = U then c {a\<in>A. k a = U} else s A)"
+  "Sup_lexord k c s A =
+  (let U = (SUP a\<in>A. k a)
+   in if \<exists>a\<in>A. k a = U then c {a\<in>A. k a = U} else s A)"
 
 lemma Sup_lexord:
   "(\<And>a S. a \<in> A \<Longrightarrow> k a = (SUP a\<in>A. k a) \<Longrightarrow> S = {a'\<in>A. k a' = k a} \<Longrightarrow> P (c S)) \<Longrightarrow> ((\<And>a. a \<in> A \<Longrightarrow> k a \<noteq> (SUP a\<in>A. k a)) \<Longrightarrow> P (s A)) \<Longrightarrow>
@@ -3194,9 +3198,9 @@
   "finite I \<Longrightarrow> I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> sets i = sets M) \<Longrightarrow> sets (sup_measure.F id I) = sets M"
   by (induction I rule: finite_ne_induct) (simp_all add: sets_sup)
 
-definition%important Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
-where
-  "Sup_measure' M = measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
+definition%important Sup_measure' :: "'a measure set \<Rightarrow> 'a measure" where
+"Sup_measure' M =
+  measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
     (\<lambda>X. (SUP P\<in>{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
 
 lemma space_Sup_measure'2: "space (Sup_measure' M) = (\<Union>m\<in>M. space m)"
@@ -3265,21 +3269,20 @@
     using assms * by auto
 qed (rule UN_space_closed)
 
-definition%important Sup_measure :: "'a measure set \<Rightarrow> 'a measure"
-where
-  "Sup_measure = Sup_lexord space (Sup_lexord sets Sup_measure'
-    (\<lambda>U. sigma (\<Union>u\<in>U. space u) (\<Union>u\<in>U. sets u))) (\<lambda>U. sigma (\<Union>u\<in>U. space u) {})"
-
-definition%important Inf_measure :: "'a measure set \<Rightarrow> 'a measure"
-where
+definition%important Sup_measure :: "'a measure set \<Rightarrow> 'a measure" where
+"Sup_measure =
+  Sup_lexord space
+    (Sup_lexord sets Sup_measure'
+      (\<lambda>U. sigma (\<Union>u\<in>U. space u) (\<Union>u\<in>U. sets u)))
+    (\<lambda>U. sigma (\<Union>u\<in>U. space u) {})"
+
+definition%important Inf_measure :: "'a measure set \<Rightarrow> 'a measure" where
   "Inf_measure A = Sup {x. \<forall>a\<in>A. x \<le> a}"
 
-definition%important inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
-where
+definition%important inf_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure" where
   "inf_measure a b = Inf {a, b}"
 
-definition%important top_measure :: "'a measure"
-where
+definition%important top_measure :: "'a measure" where
   "top_measure = Inf {}"
 
 instance
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -2058,7 +2058,7 @@
       by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm)
   qed
   then show ?thesis
-    unfolding nn_integral_def_finite by (simp cong del: SUP_cong_strong)
+    unfolding nn_integral_def_finite by (simp cong del: SUP_cong_simp)
 qed
 
 lemma nn_integral_count_space_indicator:
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -436,10 +436,10 @@
   by (auto simp add: binary_def)
 
 lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
-  by (simp add: range_binary_eq cong del: SUP_cong_strong)
+  by (simp add: range_binary_eq cong del: SUP_cong_simp)
 
 lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
-  by (simp add: range_binary_eq cong del: INF_cong_strong)
+  by (simp add: range_binary_eq cong del: INF_cong_simp)
 
 lemma sigma_algebra_iff2:
      "sigma_algebra \<Omega> M \<longleftrightarrow>
@@ -802,7 +802,7 @@
 
 subsubsection%unimportant \<open>Ring generated by a semiring\<close>
 
-definition (in semiring_of_sets)
+definition (in semiring_of_sets) generated_ring :: "'a set set" where
   "generated_ring = { \<Union>C | C. C \<subseteq> M \<and> finite C \<and> disjoint C }"
 
 lemma (in semiring_of_sets) generated_ringE[elim?]:
@@ -943,11 +943,11 @@
   done
 
 lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
-  by (simp add: range_binaryset_eq cong del: SUP_cong_strong)
+  by (simp add: range_binaryset_eq cong del: SUP_cong_simp)
 
 subsubsection \<open>Closed CDI\<close>
 
-definition%important closed_cdi where
+definition%important closed_cdi :: "'a set \<Rightarrow> 'a set set \<Rightarrow> bool" where
   "closed_cdi \<Omega> M \<longleftrightarrow>
    M \<subseteq> Pow \<Omega> &
    (\<forall>s \<in> M. \<Omega> - s \<in> M) &
@@ -1181,16 +1181,16 @@
 
 subsubsection \<open>Dynkin systems\<close>
 
-locale%important dynkin_system = subset_class +
+locale%important Dynkin_system = subset_class +
   assumes space: "\<Omega> \<in> M"
     and   compl[intro!]: "\<And>A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M"
     and   UN[intro!]: "\<And>A. disjoint_family A \<Longrightarrow> range A \<subseteq> M
                            \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
 
-lemma (in dynkin_system) empty[intro, simp]: "{} \<in> M"
+lemma (in Dynkin_system) empty[intro, simp]: "{} \<in> M"
   using space compl[of "\<Omega>"] by simp
 
-lemma (in dynkin_system) diff:
+lemma (in Dynkin_system) diff:
   assumes sets: "D \<in> M" "E \<in> M" and "D \<subseteq> E"
   shows "E - D \<in> M"
 proof -
@@ -1209,41 +1209,42 @@
   finally show ?thesis .
 qed
 
-lemma dynkin_systemI:
+lemma Dynkin_systemI:
   assumes "\<And> A. A \<in> M \<Longrightarrow> A \<subseteq> \<Omega>" "\<Omega> \<in> M"
   assumes "\<And> A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M"
   assumes "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> M
           \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
-  shows "dynkin_system \<Omega> M"
-  using assms by (auto simp: dynkin_system_def dynkin_system_axioms_def subset_class_def)
+  shows "Dynkin_system \<Omega> M"
+  using assms by (auto simp: Dynkin_system_def Dynkin_system_axioms_def subset_class_def)
 
-lemma dynkin_systemI':
+lemma Dynkin_systemI':
   assumes 1: "\<And> A. A \<in> M \<Longrightarrow> A \<subseteq> \<Omega>"
   assumes empty: "{} \<in> M"
   assumes Diff: "\<And> A. A \<in> M \<Longrightarrow> \<Omega> - A \<in> M"
   assumes 2: "\<And> A. disjoint_family A \<Longrightarrow> range A \<subseteq> M
           \<Longrightarrow> (\<Union>i::nat. A i) \<in> M"
-  shows "dynkin_system \<Omega> M"
+  shows "Dynkin_system \<Omega> M"
 proof -
   from Diff[OF empty] have "\<Omega> \<in> M" by auto
   from 1 this Diff 2 show ?thesis
-    by (intro dynkin_systemI) auto
+    by (intro Dynkin_systemI) auto
 qed
 
-lemma dynkin_system_trivial:
-  shows "dynkin_system A (Pow A)"
-  by (rule dynkin_systemI) auto
+lemma Dynkin_system_trivial:
+  shows "Dynkin_system A (Pow A)"
+  by (rule Dynkin_systemI) auto
 
-lemma sigma_algebra_imp_dynkin_system:
-  assumes "sigma_algebra \<Omega> M" shows "dynkin_system \<Omega> M"
+lemma sigma_algebra_imp_Dynkin_system:
+  assumes "sigma_algebra \<Omega> M" shows "Dynkin_system \<Omega> M"
 proof -
   interpret sigma_algebra \<Omega> M by fact
-  show ?thesis using sets_into_space by (fastforce intro!: dynkin_systemI)
+  show ?thesis using sets_into_space by (fastforce intro!: Dynkin_systemI)
 qed
 
 subsubsection "Intersection sets systems"
 
-definition%important "Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
+definition%important Int_stable :: "'a set set \<Rightarrow> bool" where
+"Int_stable M \<longleftrightarrow> (\<forall> a \<in> M. \<forall> b \<in> M. a \<inter> b \<in> M)"
 
 lemma (in algebra) Int_stable: "Int_stable M"
   unfolding Int_stable_def by auto
@@ -1260,7 +1261,7 @@
   "Int_stable M \<Longrightarrow> a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b \<in> M"
   unfolding Int_stable_def by auto
 
-lemma (in dynkin_system) sigma_algebra_eq_Int_stable:
+lemma (in Dynkin_system) sigma_algebra_eq_Int_stable:
   "sigma_algebra \<Omega> M \<longleftrightarrow> Int_stable M"
 proof
   assume "sigma_algebra \<Omega> M" then show "Int_stable M"
@@ -1283,48 +1284,48 @@
 
 subsubsection "Smallest Dynkin systems"
 
-definition%important dynkin where
-  "dynkin \<Omega> M =  (\<Inter>{D. dynkin_system \<Omega> D \<and> M \<subseteq> D})"
+definition%important Dynkin :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" where
+  "Dynkin \<Omega> M =  (\<Inter>{D. Dynkin_system \<Omega> D \<and> M \<subseteq> D})"
 
-lemma dynkin_system_dynkin:
+lemma Dynkin_system_Dynkin:
   assumes "M \<subseteq> Pow (\<Omega>)"
-  shows "dynkin_system \<Omega> (dynkin \<Omega> M)"
-proof (rule dynkin_systemI)
-  fix A assume "A \<in> dynkin \<Omega> M"
+  shows "Dynkin_system \<Omega> (Dynkin \<Omega> M)"
+proof (rule Dynkin_systemI)
+  fix A assume "A \<in> Dynkin \<Omega> M"
   moreover
-  { fix D assume "A \<in> D" and d: "dynkin_system \<Omega> D"
-    then have "A \<subseteq> \<Omega>" by (auto simp: dynkin_system_def subset_class_def) }
-  moreover have "{D. dynkin_system \<Omega> D \<and> M \<subseteq> D} \<noteq> {}"
-    using assms dynkin_system_trivial by fastforce
+  { fix D assume "A \<in> D" and d: "Dynkin_system \<Omega> D"
+    then have "A \<subseteq> \<Omega>" by (auto simp: Dynkin_system_def subset_class_def) }
+  moreover have "{D. Dynkin_system \<Omega> D \<and> M \<subseteq> D} \<noteq> {}"
+    using assms Dynkin_system_trivial by fastforce
   ultimately show "A \<subseteq> \<Omega>"
-    unfolding dynkin_def using assms
+    unfolding Dynkin_def using assms
     by auto
 next
-  show "\<Omega> \<in> dynkin \<Omega> M"
-    unfolding dynkin_def using dynkin_system.space by fastforce
+  show "\<Omega> \<in> Dynkin \<Omega> M"
+    unfolding Dynkin_def using Dynkin_system.space by fastforce
 next
-  fix A assume "A \<in> dynkin \<Omega> M"
-  then show "\<Omega> - A \<in> dynkin \<Omega> M"
-    unfolding dynkin_def using dynkin_system.compl by force
+  fix A assume "A \<in> Dynkin \<Omega> M"
+  then show "\<Omega> - A \<in> Dynkin \<Omega> M"
+    unfolding Dynkin_def using Dynkin_system.compl by force
 next
   fix A :: "nat \<Rightarrow> 'a set"
-  assume A: "disjoint_family A" "range A \<subseteq> dynkin \<Omega> M"
-  show "(\<Union>i. A i) \<in> dynkin \<Omega> M" unfolding dynkin_def
+  assume A: "disjoint_family A" "range A \<subseteq> Dynkin \<Omega> M"
+  show "(\<Union>i. A i) \<in> Dynkin \<Omega> M" unfolding Dynkin_def
   proof (simp, safe)
-    fix D assume "dynkin_system \<Omega> D" "M \<subseteq> D"
+    fix D assume "Dynkin_system \<Omega> D" "M \<subseteq> D"
     with A have "(\<Union>i. A i) \<in> D"
-      by (intro dynkin_system.UN) (auto simp: dynkin_def)
+      by (intro Dynkin_system.UN) (auto simp: Dynkin_def)
     then show "(\<Union>i. A i) \<in> D" by auto
   qed
 qed
 
-lemma dynkin_Basic[intro]: "A \<in> M \<Longrightarrow> A \<in> dynkin \<Omega> M"
-  unfolding dynkin_def by auto
+lemma Dynkin_Basic[intro]: "A \<in> M \<Longrightarrow> A \<in> Dynkin \<Omega> M"
+  unfolding Dynkin_def by auto
 
-lemma (in dynkin_system) restricted_dynkin_system:
+lemma (in Dynkin_system) restricted_Dynkin_system:
   assumes "D \<in> M"
-  shows "dynkin_system \<Omega> {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> D \<in> M}"
-proof (rule dynkin_systemI, simp_all)
+  shows "Dynkin_system \<Omega> {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> D \<in> M}"
+proof (rule Dynkin_systemI, simp_all)
   have "\<Omega> \<inter> D = D"
     using \<open>D \<in> M\<close> sets_into_space by auto
   then show "\<Omega> \<inter> D \<in> M"
@@ -1345,87 +1346,87 @@
     by (auto simp del: UN_simps)
 qed
 
-lemma (in dynkin_system) dynkin_subset:
+lemma (in Dynkin_system) Dynkin_subset:
   assumes "N \<subseteq> M"
-  shows "dynkin \<Omega> N \<subseteq> M"
+  shows "Dynkin \<Omega> N \<subseteq> M"
 proof -
-  have "dynkin_system \<Omega> M" ..
-  then have "dynkin_system \<Omega> M"
-    using assms unfolding dynkin_system_def dynkin_system_axioms_def subset_class_def by simp
-  with \<open>N \<subseteq> M\<close> show ?thesis by (auto simp add: dynkin_def)
+  have "Dynkin_system \<Omega> M" ..
+  then have "Dynkin_system \<Omega> M"
+    using assms unfolding Dynkin_system_def Dynkin_system_axioms_def subset_class_def by simp
+  with \<open>N \<subseteq> M\<close> show ?thesis by (auto simp add: Dynkin_def)
 qed
 
-lemma sigma_eq_dynkin:
+lemma sigma_eq_Dynkin:
   assumes sets: "M \<subseteq> Pow \<Omega>"
   assumes "Int_stable M"
-  shows "sigma_sets \<Omega> M = dynkin \<Omega> M"
+  shows "sigma_sets \<Omega> M = Dynkin \<Omega> M"
 proof -
-  have "dynkin \<Omega> M \<subseteq> sigma_sets (\<Omega>) (M)"
-    using sigma_algebra_imp_dynkin_system
-    unfolding dynkin_def sigma_sets_least_sigma_algebra[OF sets] by auto
+  have "Dynkin \<Omega> M \<subseteq> sigma_sets (\<Omega>) (M)"
+    using sigma_algebra_imp_Dynkin_system
+    unfolding Dynkin_def sigma_sets_least_sigma_algebra[OF sets] by auto
   moreover
-  interpret dynkin_system \<Omega> "dynkin \<Omega> M"
-    using dynkin_system_dynkin[OF sets] .
-  have "sigma_algebra \<Omega> (dynkin \<Omega> M)"
+  interpret Dynkin_system \<Omega> "Dynkin \<Omega> M"
+    using Dynkin_system_Dynkin[OF sets] .
+  have "sigma_algebra \<Omega> (Dynkin \<Omega> M)"
     unfolding sigma_algebra_eq_Int_stable Int_stable_def
   proof (intro ballI)
-    fix A B assume "A \<in> dynkin \<Omega> M" "B \<in> dynkin \<Omega> M"
-    let ?D = "\<lambda>E. {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> E \<in> dynkin \<Omega> M}"
+    fix A B assume "A \<in> Dynkin \<Omega> M" "B \<in> Dynkin \<Omega> M"
+    let ?D = "\<lambda>E. {Q. Q \<subseteq> \<Omega> \<and> Q \<inter> E \<in> Dynkin \<Omega> M}"
     have "M \<subseteq> ?D B"
     proof
       fix E assume "E \<in> M"
-      then have "M \<subseteq> ?D E" "E \<in> dynkin \<Omega> M"
+      then have "M \<subseteq> ?D E" "E \<in> Dynkin \<Omega> M"
         using sets_into_space \<open>Int_stable M\<close> by (auto simp: Int_stable_def)
-      then have "dynkin \<Omega> M \<subseteq> ?D E"
-        using restricted_dynkin_system \<open>E \<in> dynkin \<Omega> M\<close>
-        by (intro dynkin_system.dynkin_subset) simp_all
+      then have "Dynkin \<Omega> M \<subseteq> ?D E"
+        using restricted_Dynkin_system \<open>E \<in> Dynkin \<Omega> M\<close>
+        by (intro Dynkin_system.Dynkin_subset) simp_all
       then have "B \<in> ?D E"
-        using \<open>B \<in> dynkin \<Omega> M\<close> by auto
-      then have "E \<inter> B \<in> dynkin \<Omega> M"
+        using \<open>B \<in> Dynkin \<Omega> M\<close> by auto
+      then have "E \<inter> B \<in> Dynkin \<Omega> M"
         by (subst Int_commute) simp
       then show "E \<in> ?D B"
         using sets \<open>E \<in> M\<close> by auto
     qed
-    then have "dynkin \<Omega> M \<subseteq> ?D B"
-      using restricted_dynkin_system \<open>B \<in> dynkin \<Omega> M\<close>
-      by (intro dynkin_system.dynkin_subset) simp_all
-    then show "A \<inter> B \<in> dynkin \<Omega> M"
-      using \<open>A \<in> dynkin \<Omega> M\<close> sets_into_space by auto
+    then have "Dynkin \<Omega> M \<subseteq> ?D B"
+      using restricted_Dynkin_system \<open>B \<in> Dynkin \<Omega> M\<close>
+      by (intro Dynkin_system.Dynkin_subset) simp_all
+    then show "A \<inter> B \<in> Dynkin \<Omega> M"
+      using \<open>A \<in> Dynkin \<Omega> M\<close> sets_into_space by auto
   qed
   from sigma_algebra.sigma_sets_subset[OF this, of "M"]
-  have "sigma_sets (\<Omega>) (M) \<subseteq> dynkin \<Omega> M" by auto
-  ultimately have "sigma_sets (\<Omega>) (M) = dynkin \<Omega> M" by auto
+  have "sigma_sets (\<Omega>) (M) \<subseteq> Dynkin \<Omega> M" by auto
+  ultimately have "sigma_sets (\<Omega>) (M) = Dynkin \<Omega> M" by auto
   then show ?thesis
-    by (auto simp: dynkin_def)
+    by (auto simp: Dynkin_def)
 qed
 
-lemma (in dynkin_system) dynkin_idem:
-  "dynkin \<Omega> M = M"
+lemma (in Dynkin_system) Dynkin_idem:
+  "Dynkin \<Omega> M = M"
 proof -
-  have "dynkin \<Omega> M = M"
+  have "Dynkin \<Omega> M = M"
   proof
-    show "M \<subseteq> dynkin \<Omega> M"
-      using dynkin_Basic by auto
-    show "dynkin \<Omega> M \<subseteq> M"
-      by (intro dynkin_subset) auto
+    show "M \<subseteq> Dynkin \<Omega> M"
+      using Dynkin_Basic by auto
+    show "Dynkin \<Omega> M \<subseteq> M"
+      by (intro Dynkin_subset) auto
   qed
   then show ?thesis
-    by (auto simp: dynkin_def)
+    by (auto simp: Dynkin_def)
 qed
 
-lemma (in dynkin_system) dynkin_lemma:
+lemma (in Dynkin_system) Dynkin_lemma:
   assumes "Int_stable E"
   and E: "E \<subseteq> M" "M \<subseteq> sigma_sets \<Omega> E"
   shows "sigma_sets \<Omega> E = M"
 proof -
   have "E \<subseteq> Pow \<Omega>"
     using E sets_into_space by force
-  then have *: "sigma_sets \<Omega> E = dynkin \<Omega> E"
-    using \<open>Int_stable E\<close> by (rule sigma_eq_dynkin)
-  then have "dynkin \<Omega> E = M"
-    using assms dynkin_subset[OF E(1)] by simp
+  then have *: "sigma_sets \<Omega> E = Dynkin \<Omega> E"
+    using \<open>Int_stable E\<close> by (rule sigma_eq_Dynkin)
+  then have "Dynkin \<Omega> E = M"
+    using assms Dynkin_subset[OF E(1)] by simp
   with * show ?thesis
-    using assms by (auto simp: dynkin_def)
+    using assms by (auto simp: Dynkin_def)
 qed
 
 subsubsection \<open>Induction rule for intersection-stable generators\<close>
@@ -1447,10 +1448,10 @@
   interpret sigma_algebra \<Omega> "sigma_sets \<Omega> G"
     using closed by (rule sigma_algebra_sigma_sets)
   from compl[OF _ empty] closed have space: "P \<Omega>" by simp
-  interpret dynkin_system \<Omega> ?D
+  interpret Dynkin_system \<Omega> ?D
     by standard (auto dest: sets_into_space intro!: space compl union)
   have "sigma_sets \<Omega> G = ?D"
-    by (rule dynkin_lemma) (auto simp: basic \<open>Int_stable G\<close>)
+    by (rule Dynkin_lemma) (auto simp: basic \<open>Int_stable G\<close>)
   with A show ?thesis by auto
 qed
 
@@ -1460,13 +1461,16 @@
   "positive M \<mu> \<longleftrightarrow> \<mu> {} = 0"
 
 definition%important countably_additive :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
-  "countably_additive M f \<longleftrightarrow> (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
+"countably_additive M f \<longleftrightarrow>
+  (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
     (\<Sum>i. f (A i)) = f (\<Union>i. A i))"
 
 definition%important measure_space :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> bool" where
-  "measure_space \<Omega> A \<mu> \<longleftrightarrow> sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
+"measure_space \<Omega> A \<mu> \<longleftrightarrow>
+  sigma_algebra \<Omega> A \<and> positive A \<mu> \<and> countably_additive A \<mu>"
 
-typedef%important 'a measure = "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
+typedef%important 'a measure =
+  "{(\<Omega>::'a set, A, \<mu>). (\<forall>a\<in>-A. \<mu> a = 0) \<and> measure_space \<Omega> A \<mu> }"
 proof%unimportant
   have "sigma_algebra UNIV {{}, UNIV}"
     by (auto simp: sigma_algebra_iff2)
@@ -1498,8 +1502,10 @@
 interpretation sets: sigma_algebra "space M" "sets M" for M :: "'a measure"
   using measure_space[of M] by (auto simp: measure_space_def)
 
-definition%important measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure" where
-  "measure_of \<Omega> A \<mu> = Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
+definition%important measure_of :: "'a set \<Rightarrow> 'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a measure"
+  where
+"measure_of \<Omega> A \<mu> =
+  Abs_measure (\<Omega>, if A \<subseteq> Pow \<Omega> then sigma_sets \<Omega> A else {{}, \<Omega>},
     \<lambda>a. if a \<in> sigma_sets \<Omega> A \<and> measure_space \<Omega> (sigma_sets \<Omega> A) \<mu> then \<mu> a else 0)"
 
 abbreviation "sigma \<Omega> A \<equiv> measure_of \<Omega> A (\<lambda>x. 0)"
@@ -1715,8 +1721,9 @@
 
 subsubsection \<open>Measurable functions\<close>
 
-definition%important measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>M" 60) where
-  "measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
+definition%important measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set"
+  (infixr "\<rightarrow>\<^sub>M" 60) where
+"measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
 
 lemma measurableI:
   "(\<And>x. x \<in> space M \<Longrightarrow> f x \<in> space N) \<Longrightarrow> (\<And>A. A \<in> sets N \<Longrightarrow> f -` A \<inter> space M \<in> sets M) \<Longrightarrow>
@@ -1802,7 +1809,7 @@
   unfolding measurable_def using assms
   by (simp cong: vimage_inter_cong Pi_cong add: simp_implies_def)
 
-lemma measurable_cong_strong:
+lemma measurable_cong_simp:
   "M = N \<Longrightarrow> M' = N' \<Longrightarrow> (\<And>w. w \<in> space M \<Longrightarrow> f w = g w) \<Longrightarrow>
     f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable N N'"
   by (metis measurable_cong)
@@ -1878,7 +1885,7 @@
 subsubsection \<open>Counting space\<close>
 
 definition%important count_space :: "'a set \<Rightarrow> 'a measure" where
-  "count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then of_nat (card A) else \<infinity>)"
+"count_space \<Omega> = measure_of \<Omega> (Pow \<Omega>) (\<lambda>A. if finite A then of_nat (card A) else \<infinity>)"
 
 lemma
   shows space_count_space[simp]: "space (count_space \<Omega>) = \<Omega>"
@@ -1955,7 +1962,9 @@
 
 subsubsection%unimportant \<open>Extend measure\<close>
 
-definition "extend_measure \<Omega> I G \<mu> =
+definition extend_measure :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('b \<Rightarrow> 'a set) \<Rightarrow> ('b \<Rightarrow> ennreal) \<Rightarrow> 'a measure"
+  where
+"extend_measure \<Omega> I G \<mu> =
   (if (\<exists>\<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>') \<and> \<not> (\<forall>i\<in>I. \<mu> i = 0)
       then measure_of \<Omega> (G`I) (SOME \<mu>'. (\<forall>i\<in>I. \<mu>' (G i) = \<mu> i) \<and> measure_space \<Omega> (sigma_sets \<Omega> (G`I)) \<mu>')
       else measure_of \<Omega> (G`I) (\<lambda>_. 0))"
@@ -2015,7 +2024,7 @@
 
 subsection \<open>The smallest $\sigma$-algebra regarding a function\<close>
 
-definition%important
+definition%important vimage_algebra :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b measure \<Rightarrow> 'a measure" where
   "vimage_algebra X f M = sigma X {f -` A \<inter> X | A. A \<in> sets M}"
 
 lemma space_vimage_algebra[simp]: "space (vimage_algebra X f M) = X"
@@ -2090,7 +2099,7 @@
 
 subsubsection \<open>Restricted Space Sigma Algebra\<close>
 
-definition restrict_space where
+definition restrict_space :: "'a measure \<Rightarrow> 'a set \<Rightarrow> 'a measure" where
   "restrict_space M \<Omega> = measure_of (\<Omega> \<inter> space M) (((\<inter>) \<Omega>) ` sets M) (emeasure M)"
 
 lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M"
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Complete_Lattices.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -61,7 +61,7 @@
 lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
   by (simp add: image_def)
 
-lemma INF_cong_strong [cong]:
+lemma INF_cong_simp [cong]:
   "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
   unfolding simp_implies_def by (fact INF_cong)
 
@@ -82,9 +82,9 @@
 lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
 by (fact Inf.INF_cong)
 
-lemma SUP_cong_strong [cong]:
+lemma SUP_cong_simp [cong]:
   "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
-by (fact Inf.INF_cong_strong)
+by (fact Inf.INF_cong_simp)
 
 end
 
@@ -179,19 +179,19 @@
   by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
 
 lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> \<Sqinter>(f ` A)"
-  by (simp cong del: INF_cong_strong)
+  by (simp cong del: INF_cong_simp)
 
 lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
   by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
 
 lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> \<Squnion>(f ` A)"
-  by (simp cong del: SUP_cong_strong)
+  by (simp cong del: SUP_cong_simp)
 
 lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
-  by (simp cong del: INF_cong_strong)
+  by (simp cong del: INF_cong_simp)
 
 lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
-  by (simp cong del: SUP_cong_strong)
+  by (simp cong del: SUP_cong_simp)
 
 lemma Inf_UNIV [simp]: "\<Sqinter>UNIV = \<bottom>"
   by (auto intro!: antisym Inf_lower)
@@ -437,11 +437,11 @@
 
 lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> \<Sqinter>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   using INF_eq_const [of I f c] INF_lower [of _ I f]
-  by (auto intro: antisym cong del: INF_cong_strong)
+  by (auto intro: antisym cong del: INF_cong_simp)
 
 lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> \<Squnion>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
   using SUP_eq_const [of I f c] SUP_upper [of _ I f]
-  by (auto intro: antisym cong del: SUP_cong_strong)
+  by (auto intro: antisym cong del: SUP_cong_simp)
 
 end
 
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Data_Structures/Braun_Tree.thy
--- a/src/HOL/Data_Structures/Braun_Tree.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Data_Structures/Braun_Tree.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -252,7 +252,7 @@
     by (simp add: insert_ident Icc_eq_insert_lb_nat nat_in_image braun_indices1)
   thus ?case using Node.IH even_odd_decomp[OF _ _ 3]
     by(simp add: card_image inj_on_def card_braun_indices Let_def 1 2 inj_image_eq_iff image_comp
-           cong: image_cong_strong)
+           cong: image_cong_simp)
 qed
 
 lemma braun_iff_braun_indices: "braun t \<longleftrightarrow> braun_indices t = {1..size t}"
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Hoare_Parallel/RG_Examples.thy
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -321,7 +321,7 @@
       \<lbrace>\<forall>i<n. (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and>
         (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i)\<rbrace>]"
 apply (rule Parallel)
-apply (auto cong del: INF_cong_strong SUP_cong_strong)
+apply (auto cong del: INF_cong_simp SUP_cong_simp)
 apply force
 apply (rule While)
     apply force
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -188,7 +188,7 @@
 proof(cases "Y = {}")
   case True
   then show ?thesis
-    by (simp add: image_constant_conv cong del: SUP_cong_strong)
+    by (simp add: image_constant_conv cong del: SUP_cong_simp)
 next
   case False
   have chain1: "\<And>f. f \<in> Z \<Longrightarrow> Complete_Partial_Order.chain (\<le>) (f ` Y)"
@@ -518,7 +518,7 @@
 context ccpo begin
 
 lemma cont_const [simp, cont_intro]: "cont luba orda Sup (\<le>) (\<lambda>x. c)"
-by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_strong)
+by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp)
 
 lemma mcont_const [cont_intro, simp]:
   "mcont luba orda Sup (\<le>) (\<lambda>x. c)"
@@ -695,7 +695,7 @@
     hence "\<Squnion>Y \<le> bound" using chain by(auto intro: ccpo_Sup_least)
     moreover have "Y \<inter> {x. \<not> x \<le> bound} = {}" using True by auto
     ultimately show ?thesis using True Y
-      by (auto simp add: image_constant_conv cong del: c.SUP_cong_strong)
+      by (auto simp add: image_constant_conv cong del: c.SUP_cong_simp)
   next
     case False
     let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -1763,7 +1763,7 @@
   qed
 qed
 
-lemma bind_cong_strong: "M = N \<Longrightarrow> (\<And>x. x\<in>space M =simp=> f x = g x) \<Longrightarrow> bind M f = bind N g"
+lemma bind_cong_simp: "M = N \<Longrightarrow> (\<And>x. x\<in>space M =simp=> f x = g x) \<Longrightarrow> bind M f = bind N g"
   by (auto simp: simp_implies_def intro!: bind_cong)
 
 lemma sets_bind_measurable:
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Probability/Independent_Family.thy
--- a/src/HOL/Probability/Independent_Family.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Probability/Independent_Family.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -118,9 +118,9 @@
     and indep_setD_ev2: "B \<subseteq> events"
   using indep unfolding indep_set_def indep_sets_def UNIV_bool by auto
 
-lemma (in prob_space) indep_sets_dynkin:
+lemma (in prob_space) indep_sets_Dynkin:
   assumes indep: "indep_sets F I"
-  shows "indep_sets (\<lambda>i. dynkin (space M) (F i)) I"
+  shows "indep_sets (\<lambda>i. Dynkin (space M) (F i)) I"
     (is "indep_sets ?F I")
 proof (subst indep_sets_finite_index_sets, intro allI impI ballI)
   fix J assume "finite J" "J \<subseteq> I" "J \<noteq> {}"
@@ -178,8 +178,8 @@
           qed
         qed }
       note indep_sets_insert = this
-      have "dynkin_system (space M) ?D"
-      proof (rule dynkin_systemI', simp_all cong del: indep_sets_cong, safe)
+      have "Dynkin_system (space M) ?D"
+      proof (rule Dynkin_systemI', simp_all cong del: indep_sets_cong, safe)
         show "indep_sets (G(j := {{}})) K"
           by (rule indep_sets_insert) auto
       next
@@ -249,8 +249,8 @@
             by (auto dest!: sums_unique)
         qed (insert F, auto)
       qed (insert sets.sets_into_space, auto)
-      then have mono: "dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}"
-      proof (rule dynkin_system.dynkin_subset, safe)
+      then have mono: "Dynkin (space M) (G j) \<subseteq> {E \<in> events. indep_sets (G(j := {E})) K}"
+      proof (rule Dynkin_system.Dynkin_subset, safe)
         fix X assume "X \<in> G j"
         then show "X \<in> events" using G \<open>j \<in> K\<close> by auto
         from \<open>indep_sets G K\<close>
@@ -276,7 +276,7 @@
             by (intro indep_setsD[OF G(1)]) auto
         qed
       qed
-      then have "indep_sets (G(j := dynkin (space M) (G j))) K"
+      then have "indep_sets (G(j := Dynkin (space M) (G j))) K"
         by (rule indep_sets_mono_sets) (insert mono, auto)
       then show ?case
         by (rule indep_sets_mono_sets) (insert \<open>j \<in> K\<close> \<open>j \<notin> J\<close>, auto simp: G_def)
@@ -291,9 +291,9 @@
   assumes stable: "\<And>i. i \<in> I \<Longrightarrow> Int_stable (F i)"
   shows "indep_sets (\<lambda>i. sigma_sets (space M) (F i)) I"
 proof -
-  from indep_sets_dynkin[OF indep]
+  from indep_sets_Dynkin[OF indep]
   show ?thesis
-  proof (rule indep_sets_mono_sets, subst sigma_eq_dynkin, simp_all add: stable)
+  proof (rule indep_sets_mono_sets, subst sigma_eq_Dynkin, simp_all add: stable)
     fix i assume "i \<in> I"
     with indep have "F i \<subseteq> events" by (auto simp: indep_sets_def)
     with sets.sets_into_space show "F i \<subseteq> Pow (space M)" by auto
@@ -662,8 +662,8 @@
   have X_in: "X \<in> events"
     using tail_events_sets A X by auto
 
-  interpret D: dynkin_system "space M" ?D
-  proof (rule dynkin_systemI)
+  interpret D: Dynkin_system "space M" ?D
+  proof (rule Dynkin_systemI)
     fix D assume "D \<in> ?D" then show "D \<subseteq> space M"
       using sets.sets_into_space by auto
   next
@@ -739,8 +739,8 @@
       by (intro sigma_sets_subseteq UN_mono) auto
    then have "tail_events A \<subseteq> sigma_sets (space M) ?A"
       unfolding tail_events_def by auto }
-  also have "sigma_sets (space M) ?A = dynkin (space M) ?A"
-  proof (rule sigma_eq_dynkin)
+  also have "sigma_sets (space M) ?A = Dynkin (space M) ?A"
+  proof (rule sigma_eq_Dynkin)
     { fix B n assume "B \<in> sigma_sets (space M) (\<Union>m\<in>{..n}. A m)"
       then have "B \<subseteq> space M"
         by induct (insert A sets.sets_into_space[of _ M], auto) }
@@ -763,8 +763,8 @@
       then show "a \<inter> b \<in> (\<Union>n. sigma_sets (space M) (\<Union>i\<in>{..n}. A i))" by auto
     qed
   qed
-  also have "dynkin (space M) ?A \<subseteq> ?D"
-    using \<open>?A \<subseteq> ?D\<close> by (auto intro!: D.dynkin_subset)
+  also have "Dynkin (space M) ?A \<subseteq> ?D"
+    using \<open>?A \<subseteq> ?D\<close> by (auto intro!: D.Dynkin_subset)
   finally show ?thesis by auto
 qed
 
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/ROOT	Tue Jan 01 18:33:19 2019 +0100
@@ -65,7 +65,6 @@
     "HOL-Library"
     "HOL-Computational_Algebra"
   theories
-    L2_Norm
     Analysis
   document_files
     "root.tex"
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Set.thy
--- a/src/HOL/Set.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Set.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -426,7 +426,7 @@
     (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
 by (simp add: Ball_def)
 
-lemma ball_cong_strong [cong]:
+lemma ball_cong_simp [cong]:
   "\<lbrakk> A = B;  \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
     (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
 by (simp add: simp_implies_def Ball_def)
@@ -436,7 +436,7 @@
     (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
 by (simp add: Bex_def cong: conj_cong)
 
-lemma bex_cong_strong [cong]:
+lemma bex_cong_simp [cong]:
   "\<lbrakk> A = B;  \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
     (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
 by (simp add: simp_implies_def Bex_def cong: conj_cong)
@@ -939,7 +939,7 @@
 lemma image_cong: "\<lbrakk> M = N;  \<And>x. x \<in> N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> f ` M = g ` N"
 by (simp add: image_def)
 
-lemma image_cong_strong: "\<lbrakk> M = N; \<And>x. x \<in> N =simp=> f x = g x\<rbrakk> \<Longrightarrow> f ` M = g ` N"
+lemma image_cong_simp: "\<lbrakk> M = N; \<And>x. x \<in> N =simp=> f x = g x\<rbrakk> \<Longrightarrow> f ` M = g ` N"
 by (simp add: image_def simp_implies_def)
 
 lemma image_Int_subset: "f ` (A \<inter> B) \<subseteq> f ` A \<inter> f ` B"
diff -r de09a7261120 -r 2d88bf80c84f src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Jan 01 18:33:19 2019 +0100
@@ -1882,7 +1882,7 @@
   unfolding continuous_on_def
   by (intro ball_cong filterlim_cong) (auto simp: eventually_at_filter)
 
-lemma continuous_on_cong_strong:
+lemma continuous_on_cong_simp:
   "s = t \<Longrightarrow> (\<And>x. x \<in> t =simp=> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
   unfolding simp_implies_def by (rule continuous_on_cong)
 
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/General/path.ML	Tue Jan 01 18:33:19 2019 +0100
@@ -51,18 +51,20 @@
 
 local
 
-fun err_elem msg s = error (msg ^ " path element specification " ^ quote s);
+fun err_elem msg s = error (msg ^ " path element " ^ quote s);
 
-fun check_elem s =
-  if s = "" orelse s = "~" orelse s = "~~" then err_elem "Illegal" s
+val illegal_elem = ["", "~", "~~", ".", ".."];
+val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"];
+
+val check_elem = tap (fn s =>
+  if member (op =) illegal_elem s then err_elem "Illegal" s
   else
-    let
-      fun check c =
-        if exists_string (fn c' => c = c') s then
-          err_elem ("Illegal character " ^ quote c ^ " in") s
-        else ();
-      val _ = List.app check ["/", "\\", "$", ":", "\"", "'"];
-    in s end;
+    (s, ()) |-> fold_string (fn c => fn () =>
+      if ord c < 32 then
+        err_elem ("Illegal control character " ^ string_of_int (ord c) ^ " in") s
+      else if member (op =) illegal_char c then
+        err_elem ("Illegal character " ^ quote c ^ " in") s
+      else ()));
 
 in
 
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/General/path.scala	Tue Jan 01 18:33:19 2019 +0100
@@ -24,14 +24,20 @@
   private case object Parent extends Elem
 
   private def err_elem(msg: String, s: String): Nothing =
-    error(msg + " path element specification " + quote(s))
+    error(msg + " path element " + quote(s))
+
+  private val illegal_elem = Set("", "~", "~~", ".", "..")
+  private val illegal_char = "/\\$:\"'<>|?*"
 
   private def check_elem(s: String): String =
-    if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
+    if (illegal_elem.contains(s)) err_elem("Illegal", s)
     else {
-      "/\\$:\"'".iterator.foreach(c =>
-        if (s.iterator.contains(c))
-          err_elem("Illegal character " + quote(c.toString) + " in", s))
+      for (c <- s) {
+        if (c.toInt < 32)
+          err_elem("Illegal control character " + c.toInt + " in", s)
+        if (illegal_char.contains(c))
+          err_elem("Illegal character " + quote(c.toString) + " in", s)
+      }
       s
     }
 
@@ -112,6 +118,17 @@
   /* encode */
 
   val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode))
+
+
+  /* reserved names */
+
+  private val reserved_windows: Set[String] =
+    Set("CON", "PRN", "AUX", "NUL",
+      "COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9",
+      "LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9")
+
+  def is_reserved(name: String): Boolean =
+    Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a)))
 }
 
 
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/Isar/token.scala	Tue Jan 01 18:33:19 2019 +0100
@@ -328,6 +328,8 @@
   def is_system_name: Boolean =
   {
     val s = content
-    is_name && Path.is_wellformed(s) && !s.exists(Symbol.is_ascii_blank(_))
+    is_name && Path.is_wellformed(s) &&
+      !s.exists(Symbol.is_ascii_blank(_)) &&
+      !Path.is_reserved(s)
   }
 }
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Jan 01 18:33:19 2019 +0100
@@ -293,6 +293,11 @@
 
     def has_header: Boolean = header != Node.no_header
 
+    override def toString: String =
+      if (is_empty) "empty"
+      else if (get_blob.isDefined) "blob"
+      else "node"
+
     def commands: Linear_Set[Command] = _commands.commands
     def load_commands: List[Command] = _commands.load_commands
     def load_commands_changed(doc_blobs: Blobs): Boolean =
@@ -528,6 +533,7 @@
 
     def node_name: Node.Name
     def node: Node
+    def nodes: List[(Node.Name, Node)]
 
     def commands_loading: List[Command]
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
@@ -1024,6 +1030,10 @@
         val node_name: Node.Name = name
         val node: Node = version.nodes(name)
 
+        def nodes: List[(Node.Name, Node)] =
+          (node_name :: node.load_commands.flatMap(_.blobs_names)).
+            map(name => (name, version.nodes(name)))
+
         val commands_loading: List[Command] =
           if (node_name.is_theory) Nil
           else version.nodes.commands_loading(node_name)
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/PIDE/headless.scala	Tue Jan 01 18:33:19 2019 +0100
@@ -10,6 +10,7 @@
 import java.io.{File => JFile}
 
 import scala.annotation.tailrec
+import scala.collection.mutable
 
 
 object Headless
@@ -161,13 +162,17 @@
       commit_cleanup_delay: Time = default_commit_cleanup_delay,
       progress: Progress = No_Progress): Use_Theories_Result =
     {
-      val dep_theories =
+      val dependencies =
       {
         val import_names =
           theories.map(thy =>
             resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none)
-        resources.dependencies(import_names, progress = progress).check_errors.theories
+        resources.dependencies(import_names, progress = progress).check_errors
       }
+      val dep_theories = dependencies.theories
+      val dep_files =
+        dependencies.loaded_files(false).flatMap(_._2).
+          map(path => Document.Node.Name(resources.append("", path)))
 
       val use_theories_state = Synchronized(Use_Theories_State())
 
@@ -258,7 +263,7 @@
 
       try {
         session.commands_changed += consumer
-        resources.load_theories(session, id, dep_theories, progress)
+        resources.load_theories(session, id, dep_theories, dep_files, progress)
         use_theories_state.value.await_result
         check_progress.cancel
       }
@@ -341,9 +346,51 @@
     }
 
     sealed case class State(
-      required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty,
-      theories: Map[Document.Node.Name, Theory] = Map.empty)
+      blobs: Map[Document.Node.Name, Document.Blob] = Map.empty,
+      theories: Map[Document.Node.Name, Theory] = Map.empty,
+      required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty)
     {
+      /* blobs */
+
+      def doc_blobs: Document.Blobs = Document.Blobs(blobs)
+
+      def update_blobs(names: List[Document.Node.Name]): (Document.Blobs, State) =
+      {
+        val new_blobs =
+          names.flatMap(name =>
+          {
+            val bytes = Bytes.read(name.path)
+            def new_blob: Document.Blob =
+            {
+              val text = bytes.text
+              Document.Blob(bytes, text, Symbol.Text_Chunk(text), changed = true)
+            }
+            blobs.get(name) match {
+              case Some(blob) => if (blob.bytes == bytes) None else Some(name -> new_blob)
+              case None => Some(name -> new_blob)
+            }
+          })
+        val blobs1 = (blobs /: new_blobs)(_ + _)
+        val blobs2 = (blobs /: new_blobs)({ case (map, (a, b)) => map + (a -> b.unchanged) })
+        (Document.Blobs(blobs1), copy(blobs = blobs2))
+      }
+
+      def blob_edits(name: Document.Node.Name, old_blob: Option[Document.Blob])
+        : List[Document.Edit_Text] =
+      {
+        val blob = blobs.getOrElse(name, error("Missing blob " + quote(name.toString)))
+        val text_edits =
+          old_blob match {
+            case None => List(Text.Edit.insert(0, blob.source))
+            case Some(blob0) => Text.Edit.replace(0, blob0.source, blob.source)
+          }
+        if (text_edits.isEmpty) Nil
+        else List(name -> Document.Node.Blob(blob), name -> Document.Node.Edits(text_edits))
+      }
+
+
+      /* theories */
+
       lazy val theory_graph: Graph[Document.Node.Name, Unit] =
       {
         val entries =
@@ -389,7 +436,7 @@
             val edits = theory1.node_edits(Some(theory))
             (edits, (node_name, theory1))
           }
-        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
+        session.update(doc_blobs, theory_edits.flatMap(_._1))
         st1.update_theories(theory_edits.map(_._2))
       }
 
@@ -403,7 +450,7 @@
         val (retained, purged) = all_nodes.partition(retain)
 
         val purge_edits = purged.flatMap(name => theories(name).purge_edits)
-        session.update(Document.Blobs.empty, purge_edits)
+        session.update(doc_blobs, purge_edits)
 
         ((purged, retained), remove_theories(purged))
       }
@@ -475,6 +522,7 @@
       session: Session,
       id: UUID.T,
       dep_theories: List[Document.Node.Name],
+      dep_files: List[Document.Node.Name],
       progress: Progress)
     {
       val loaded_theories =
@@ -494,7 +542,7 @@
 
       state.change(st =>
         {
-          val st1 = st.insert_required(id, dep_theories)
+          val (doc_blobs1, st1) = st.insert_required(id, dep_theories).update_blobs(dep_files)
           val theory_edits =
             for (theory <- loaded_theories)
             yield {
@@ -503,7 +551,11 @@
               val edits = theory1.node_edits(st1.theories.get(node_name))
               (edits, (node_name, theory1))
             }
-          session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
+          val file_edits =
+            for { node_name <- dep_files if doc_blobs1.changed(node_name) }
+            yield st1.blob_edits(node_name, st.blobs.get(node_name))
+
+          session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten)
           st1.update_theories(theory_edits.map(_._2))
         })
     }
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Jan 01 18:33:19 2019 +0100
@@ -45,6 +45,7 @@
   val refN: string
   val completionN: string val completion: T
   val no_completionN: string val no_completion: T
+  val updateN: string val update: T
   val lineN: string
   val end_lineN: string
   val offsetN: string
@@ -336,6 +337,8 @@
 val (completionN, completion) = markup_elem "completion";
 val (no_completionN, no_completion) = markup_elem "no_completion";
 
+val (updateN, update) = markup_elem "update";
+
 
 (* position *)
 
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Jan 01 18:33:19 2019 +0100
@@ -115,6 +115,8 @@
   val COMPLETION = "completion"
   val NO_COMPLETION = "no_completion"
 
+  val UPDATE = "update"
+
 
   /* position */
 
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/PIDE/resources.scala	Tue Jan 01 18:33:19 2019 +0100
@@ -90,11 +90,12 @@
     }
   }
 
-  def pure_files(syntax: Outer_Syntax, dir: Path): List[Path] =
+  def pure_files(syntax: Outer_Syntax): List[Path] =
   {
+    val pure_dir = Path.explode("~~/src/Pure")
     val roots =
       for { (name, _) <- Thy_Header.ml_roots }
-      yield (dir + Path.explode(name)).expand
+      yield (pure_dir + Path.explode(name)).expand
     val files =
       for {
         (path, (_, theory)) <- roots zip Thy_Header.ml_roots
@@ -344,11 +345,20 @@
         graph2.map_node(name, _ => syntax)
       })
 
-    def loaded_files: List[(String, List[Path])] =
+    def loaded_files(pure: Boolean): List[(String, List[Path])] =
     {
-      theories.map(_.theory) zip
-        Par_List.map((e: () => List[Path]) => e(),
-          theories.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
+      val loaded_files =
+        theories.map(_.theory) zip
+          Par_List.map((e: () => List[Path]) => e(),
+            theories.map(name =>
+              resources.loaded_files(loaded_theories.get_node(name.theory), name)))
+
+      if (pure) {
+        val pure_files = resources.pure_files(overall_syntax)
+        loaded_files.map({ case (name, files) =>
+          (name, if (name == Thy_Header.PURE) pure_files ::: files else files) })
+      }
+      else loaded_files
     }
 
     def imported_files: List[Path] =
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Tue Jan 01 18:33:19 2019 +0100
@@ -155,6 +155,7 @@
   Present.isabelle_tool,
   Profiling_Report.isabelle_tool,
   Server.isabelle_tool,
+  Update.isabelle_tool,
   Update_Cartouches.isabelle_tool,
   Update_Comments.isabelle_tool,
   Update_Header.isabelle_tool,
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Jan 01 18:33:19 2019 +0100
@@ -303,14 +303,7 @@
 
             val theory_files = dependencies.theories.map(_.path)
             val loaded_files =
-              if (inlined_files) {
-                if (Sessions.is_pure(info.name)) {
-                  val pure_files = resources.pure_files(overall_syntax, info.dir)
-                  dependencies.loaded_files.map({ case (name, files) =>
-                    (name, if (name == Thy_Header.PURE) pure_files ::: files else files) })
-                }
-                else dependencies.loaded_files
-              }
+              if (inlined_files) dependencies.loaded_files(Sessions.is_pure(info.name))
               else Nil
 
             val session_files =
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Jan 01 18:33:19 2019 +0100
@@ -301,7 +301,7 @@
   {
     val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
 
-    def get_blob(name: Document.Node.Name) =
+    def get_blob(name: Document.Node.Name): Option[Document.Blob] =
       doc_blobs.get(name) orElse previous.nodes(name).get_blob
 
     def can_import(name: Document.Node.Name): Boolean =
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/Tools/update.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/update.scala	Tue Jan 01 18:33:19 2019 +0100
@@ -0,0 +1,132 @@
+/*  Title:      Pure/Tools/update.scala
+    Author:     Makarius
+
+Update theory sources based on PIDE markup.
+*/
+
+package isabelle
+
+
+object Update
+{
+  def update(options: Options, logic: String,
+    progress: Progress = No_Progress,
+    log: Logger = No_Logger,
+    dirs: List[Path] = Nil,
+    select_dirs: List[Path] = Nil,
+    system_mode: Boolean = false,
+    selection: Sessions.Selection = Sessions.Selection.empty)
+  {
+    Build.build_logic(options, logic, build_heap = true, progress = progress,
+      dirs = dirs ::: select_dirs, system_mode = system_mode, strict = true)
+
+    val dump_options = Dump.make_options(options)
+
+    val deps =
+      Dump.dependencies(dump_options, progress = progress,
+        dirs = dirs, select_dirs = select_dirs, selection = selection)._1
+
+    val resources =
+      Headless.Resources.make(dump_options, logic, progress = progress, log = log,
+        session_dirs = dirs ::: select_dirs,
+        include_sessions = deps.sessions_structure.imports_topological_order)
+
+    def update_xml(xml: XML.Body): XML.Body =
+      xml flatMap {
+        case XML.Wrapped_Elem(markup, body1, body2) =>
+          if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2)
+        case XML.Elem(_, body) => update_xml(body)
+        case t => List(t)
+      }
+
+    Dump.session(deps, resources, progress = progress,
+      process_theory =
+        (deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status) =>
+        {
+          for ((node_name, node) <- snapshot.nodes) {
+            val xml =
+              snapshot.state.markup_to_XML(snapshot.version, node_name,
+                Text.Range.full, Markup.Elements(Markup.UPDATE))
+
+            val source1 = Symbol.encode(XML.content(update_xml(xml)))
+            if (source1 != Symbol.encode(node.source)) {
+              progress.echo("Updating " + node_name.path)
+              File.write(node_name.path, source1)
+            }
+          }
+        })
+  }
+
+
+  /* Isabelle tool wrapper */
+
+  val isabelle_tool =
+    Isabelle_Tool("update", "update theory sources based on PIDE markup", args =>
+    {
+      var base_sessions: List[String] = Nil
+      var select_dirs: List[Path] = Nil
+      var requirements = false
+      var exclude_session_groups: List[String] = Nil
+      var all_sessions = false
+      var dirs: List[Path] = Nil
+      var session_groups: List[String] = Nil
+      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
+      var options = Options.init()
+      var system_mode = false
+      var verbose = false
+      var exclude_sessions: List[String] = Nil
+
+      val getopts = Getopts("""
+Usage: isabelle update [OPTIONS] [SESSIONS ...]
+
+  Options are:
+    -B NAME      include session NAME and all descendants
+    -D DIR       include session directory and select its sessions
+    -R           operate on requirements of selected sessions
+    -X NAME      exclude sessions from group NAME and all descendants
+    -a           select all sessions
+    -d DIR       include session directory
+    -g NAME      select session group NAME
+    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -s           system build mode for logic image
+    -u OPT       overide update option: shortcut for "-o update_OPT"
+    -v           verbose
+    -x NAME      exclude session NAME and all descendants
+
+  Update theory sources based on PIDE markup.
+""",
+      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
+      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+      "R" -> (_ => requirements = true),
+      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+      "a" -> (_ => all_sessions = true),
+      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+      "l:" -> (arg => logic = arg),
+      "o:" -> (arg => options = options + arg),
+      "s" -> (_ => system_mode = true),
+      "u:" -> (arg => options = options + ("update_" + arg)),
+      "v" -> (_ => verbose = true),
+      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+
+      val sessions = getopts(args)
+
+      val progress = new Console_Progress(verbose = verbose)
+
+      progress.interrupt_handler {
+        update(options, logic,
+          progress = progress,
+          dirs = dirs,
+          select_dirs = select_dirs,
+          selection = Sessions.Selection(
+            requirements = requirements,
+            all_sessions = all_sessions,
+            base_sessions = base_sessions,
+            exclude_session_groups = exclude_session_groups,
+            exclude_sessions = exclude_sessions,
+            session_groups = session_groups,
+            sessions = sessions))
+      }
+    })
+}
diff -r de09a7261120 -r 2d88bf80c84f src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Pure/build-jars	Tue Jan 01 18:33:19 2019 +0100
@@ -160,6 +160,7 @@
   Tools/simplifier_trace.scala
   Tools/spell_checker.scala
   Tools/task_statistics.scala
+  Tools/update.scala
   Tools/update_cartouches.scala
   Tools/update_comments.scala
   Tools/update_header.scala
diff -r de09a7261120 -r 2d88bf80c84f src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Tue Jan 01 17:04:53 2019 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Tue Jan 01 18:33:19 2019 +0100
@@ -144,7 +144,7 @@
 
   def get_blob: Option[Document.Blob] =
     if (is_theory) None
-    else Some((Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)))
+    else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
 
 
   /* bibtex entries */