# HG changeset patch
# User paulson
# Date 1537795997 -3600
# Node ID 697789794af15e1ecafa77e214b996e0a5455ea4
# Parent  8c240fdeffcb4b8d1364a0d1c2ada8e4d03379f2# Parent  c9ea9290880f2bbf92e873bb874ffa9ae7e5826a
merged

diff -r c9ea9290880f -r 697789794af1 NEWS
--- a/NEWS	Mon Sep 24 14:33:08 2018 +0100
+++ b/NEWS	Mon Sep 24 14:33:17 2018 +0100
@@ -7,11 +7,10 @@
 New in this Isabelle version
 ----------------------------
 
-*** System ***
-
-* Isabelle server command "use_theories" supports "nodes_status_delay"
-for continuous output of node status information. The time interval is
-specified in seconds; a negative value means it is disabled (default).
+*** General ***
+
+* Old-style inner comments (* ... *) within the term language are no
+longer supported (legacy feature in Isabelle2018).
 
 
 *** Isar ***
@@ -19,6 +18,10 @@
 * More robust treatment of structural errors: begin/end blocks take
 precedence over goal/proof.
 
+* Implicit cases goal1, goal2, goal3, etc. have been discontinued
+(legacy feature since Isabelle2016).
+
+
 
 *** HOL ***
 
@@ -35,6 +38,9 @@
 and prod_mset.swap, similarly to sum.swap and prod.swap.
 INCOMPATIBILITY.
 
+* Theory "HOL-Library.Multiset": the <Union># operator now has the same
+precedence as any other prefix function symbol.
+
 
 *** ML ***
 
@@ -64,7 +70,11 @@
 
 *** System ***
 
-* Isabelle Server message "use_theories" terminates more robustly in the
+* Isabelle server command "use_theories" supports "nodes_status_delay"
+for continuous output of node status information. The time interval is
+specified in seconds; a negative value means it is disabled (default).
+
+* Isabelle Server command "use_theories" terminates more robustly in the
 presence of structurally broken sources: full consolidation of theories
 is no longer required.
 
diff -r c9ea9290880f -r 697789794af1 src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Mon Sep 24 14:33:17 2018 +0100
@@ -150,11 +150,10 @@
   blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim "\<close>"}''. Note that the rendering
   of cartouche delimiters is usually like this: ``\<open>\<open> \<dots> \<close>\<close>''.
 
-  Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested, although
-  the user-interface might prevent this. Note that this form indicates source
-  comments only, which are stripped after lexical analysis of the input. The
-  Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are considered as
-  part of the text (see \secref{sec:comments}).
+  Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested: the text is
+  removed after lexical analysis of the input and thus not suitable for
+  documentation. The Isar syntax also provides proper \<^emph>\<open>document comments\<close>
+  that are considered as part of the text (see \secref{sec:comments}).
 
   Common mathematical symbols such as \<open>\<forall>\<close> are represented in Isabelle as \<^verbatim>\<open>\<forall>\<close>.
   There are infinitely many Isabelle symbols like this, although proper
diff -r c9ea9290880f -r 697789794af1 src/HOL/Analysis/Function_Topology.thy
--- a/src/HOL/Analysis/Function_Topology.thy	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy	Mon Sep 24 14:33:17 2018 +0100
@@ -1,9 +1,9 @@
-(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
+(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr with additions from LCP
     License: BSD
 *)
 
 theory Function_Topology
-imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure
+imports Topology_Euclidean_Space Bounded_Linear_Function Finite_Product_Measure 
 begin
 
 
@@ -94,13 +94,12 @@
 using assms(3) apply (induct rule: generate_topology_on.induct)
 using assms(1) assms(2) unfolding istopology_def by auto
 
-definition%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
-  where "topology_generated_by S = topology (generate_topology_on S)"
+abbreviation%unimportant topology_generated_by::"('a set set) \<Rightarrow> ('a topology)"
+  where "topology_generated_by S \<equiv> topology (generate_topology_on S)"
 
 lemma%unimportant openin_topology_generated_by_iff:
   "openin (topology_generated_by S) s \<longleftrightarrow> generate_topology_on S s"
-using topology_inverse'[OF istopology_generate_topology_on[of S]]
-unfolding topology_generated_by_def by simp
+  using topology_inverse'[OF istopology_generate_topology_on[of S]] by simp
 
 lemma%unimportant openin_topology_generated_by:
   "openin (topology_generated_by S) s \<Longrightarrow> generate_topology_on S s"
@@ -127,6 +126,138 @@
   "s \<in> S \<Longrightarrow> openin (topology_generated_by S) s"
 by%unimportant (simp only: openin_topology_generated_by_iff, auto simp: generate_topology_on.Basis)
 
+lemma generate_topology_on_Inter:
+  "\<lbrakk>finite \<F>; \<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on \<S> K; \<F> \<noteq> {}\<rbrakk> \<Longrightarrow> generate_topology_on \<S> (\<Inter>\<F>)"
+  by (induction \<F> rule: finite_induct; force intro: generate_topology_on.intros)
+
+subsection\<open>Topology bases and sub-bases\<close>
+
+lemma istopology_base_alt:
+   "istopology (arbitrary union_of P) \<longleftrightarrow>
+    (\<forall>S T. (arbitrary union_of P) S \<and> (arbitrary union_of P) T
+           \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
+  by (simp add: istopology_def) (blast intro: arbitrary_union_of_Union)
+
+lemma istopology_base_eq:
+   "istopology (arbitrary union_of P) \<longleftrightarrow>
+    (\<forall>S T. P S \<and> P T \<longrightarrow> (arbitrary union_of P) (S \<inter> T))"
+  by (simp add: istopology_base_alt arbitrary_union_of_Int_eq)
+
+lemma istopology_base:
+   "(\<And>S T. \<lbrakk>P S; P T\<rbrakk> \<Longrightarrow> P(S \<inter> T)) \<Longrightarrow> istopology (arbitrary union_of P)"
+  by (simp add: arbitrary_def istopology_base_eq union_of_inc)
+
+lemma openin_topology_base_unique:
+   "openin X = arbitrary union_of P \<longleftrightarrow>
+        (\<forall>V. P V \<longrightarrow> openin X V) \<and> (\<forall>U x. openin X U \<and> x \<in> U \<longrightarrow> (\<exists>V. P V \<and> x \<in> V \<and> V \<subseteq> U))"
+   (is "?lhs = ?rhs")
+proof
+  assume ?lhs
+  then show ?rhs
+    by (auto simp: union_of_def arbitrary_def)
+next
+  assume R: ?rhs
+  then have *: "\<exists>\<U>\<subseteq>Collect P. \<Union>\<U> = S" if "openin X S" for S
+    using that by (rule_tac x="{V. P V \<and> V \<subseteq> S}" in exI) fastforce
+  from R show ?lhs
+    by (fastforce simp add: union_of_def arbitrary_def intro: *)
+qed
+
+lemma topology_base_unique:
+   "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S;
+     \<And>U x. \<lbrakk>openin X U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>B. P B \<and> x \<in> B \<and> B \<subseteq> U\<rbrakk>
+    \<Longrightarrow> topology(arbitrary union_of P) = X"
+  by (metis openin_topology_base_unique openin_inverse [of X])
+
+lemma topology_bases_eq_aux:
+   "\<lbrakk>(arbitrary union_of P) S;
+     \<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U\<rbrakk>
+        \<Longrightarrow> (arbitrary union_of Q) S"
+  by (metis arbitrary_union_of_alt arbitrary_union_of_idempot)
+
+lemma topology_bases_eq:
+   "\<lbrakk>\<And>U x. \<lbrakk>P U; x \<in> U\<rbrakk> \<Longrightarrow> \<exists>V. Q V \<and> x \<in> V \<and> V \<subseteq> U;
+    \<And>V x. \<lbrakk>Q V; x \<in> V\<rbrakk> \<Longrightarrow> \<exists>U. P U \<and> x \<in> U \<and> U \<subseteq> V\<rbrakk>
+        \<Longrightarrow> topology (arbitrary union_of P) =
+            topology (arbitrary union_of Q)"
+  by (fastforce intro:  arg_cong [where f=topology]  elim: topology_bases_eq_aux)
+
+lemma istopology_subbase:
+   "istopology (arbitrary union_of (finite intersection_of P relative_to S))"
+  by (simp add: finite_intersection_of_Int istopology_base relative_to_Int)
+
+lemma openin_subbase:
+  "openin (topology (arbitrary union_of (finite intersection_of B relative_to U))) S
+   \<longleftrightarrow> (arbitrary union_of (finite intersection_of B relative_to U)) S"
+  by (simp add: istopology_subbase topology_inverse')
+
+lemma topspace_subbase [simp]:
+   "topspace(topology (arbitrary union_of (finite intersection_of B relative_to U))) = U" (is "?lhs = _")
+proof
+  show "?lhs \<subseteq> U"
+    by (metis arbitrary_union_of_relative_to openin_subbase openin_topspace relative_to_imp_subset)
+  show "U \<subseteq> ?lhs"
+    by (metis arbitrary_union_of_inc finite_intersection_of_empty inf.orderE istopology_subbase 
+              openin_subset relative_to_inc subset_UNIV topology_inverse')
+qed
+
+lemma minimal_topology_subbase:
+   "\<lbrakk>\<And>S. P S \<Longrightarrow> openin X S; openin X U;
+     openin(topology(arbitrary union_of (finite intersection_of P relative_to U))) S\<rbrakk>
+    \<Longrightarrow> openin X S"
+  apply (simp add: istopology_subbase topology_inverse)
+  apply (simp add: union_of_def intersection_of_def relative_to_def)
+  apply (blast intro: openin_Int_Inter)
+  done
+
+lemma istopology_subbase_UNIV:
+   "istopology (arbitrary union_of (finite intersection_of P))"
+  by (simp add: istopology_base finite_intersection_of_Int)
+
+
+lemma generate_topology_on_eq:
+  "generate_topology_on S = arbitrary union_of finite' intersection_of (\<lambda>x. x \<in> S)" (is "?lhs = ?rhs")
+proof (intro ext iffI)
+  fix A
+  assume "?lhs A"
+  then show "?rhs A"
+  proof induction
+    case (Int a b)
+    then show ?case
+      by (metis (mono_tags, lifting) istopology_base_alt finite'_intersection_of_Int istopology_base)
+  next
+    case (UN K)
+    then show ?case
+      by (simp add: arbitrary_union_of_Union)
+  next
+    case (Basis s)
+    then show ?case
+      by (simp add: Sup_upper arbitrary_union_of_inc finite'_intersection_of_inc relative_to_subset)
+  qed auto
+next
+  fix A
+  assume "?rhs A"
+  then obtain \<U> where \<U>: "\<And>T. T \<in> \<U> \<Longrightarrow> \<exists>\<F>. finite' \<F> \<and> \<F> \<subseteq> S \<and> \<Inter>\<F> = T" and eq: "A = \<Union>\<U>"
+    unfolding union_of_def intersection_of_def by auto
+  show "?lhs A"
+    unfolding eq
+  proof (rule generate_topology_on.UN)
+    fix T
+    assume "T \<in> \<U>"
+    with \<U> obtain \<F> where "finite' \<F>" "\<F> \<subseteq> S" "\<Inter>\<F> = T"
+      by blast
+    have "generate_topology_on S (\<Inter>\<F>)"
+    proof (rule generate_topology_on_Inter)
+      show "finite \<F>" "\<F> \<noteq> {}"
+        by (auto simp: \<open>finite' \<F>\<close>)
+      show "\<And>K. K \<in> \<F> \<Longrightarrow> generate_topology_on S K"
+        by (metis \<open>\<F> \<subseteq> S\<close> generate_topology_on.simps subset_iff)
+    qed
+    then show "generate_topology_on S T"
+      using \<open>\<Inter>\<F> = T\<close> by blast
+  qed
+qed
+
 subsubsection%important \<open>Continuity\<close>
 
 text \<open>We will need to deal with continuous maps in terms of topologies and not in terms
@@ -315,11 +446,113 @@
 text \<open>The total set of the product topology is the product of the total sets
 along each coordinate.\<close>
 
-lemma%important product_topology_topspace:
+proposition product_topology:
+  "product_topology X I =
+   topology
+    (arbitrary union_of
+       ((finite intersection_of
+        (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
+        relative_to (\<Pi>\<^sub>E i\<in>I. topspace (X i))))"
+  (is "_ = topology (_ union_of ((_ intersection_of ?\<Psi>) relative_to ?TOP))")
+proof -
+  let ?\<Omega> = "(\<lambda>F. \<exists>Y. F = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)})"
+  have *: "(finite' intersection_of ?\<Omega>) A = (finite intersection_of ?\<Psi> relative_to ?TOP) A" for A
+  proof -
+    have 1: "\<exists>U. (\<exists>\<U>. finite \<U> \<and> \<U> \<subseteq> Collect ?\<Psi> \<and> \<Inter>\<U> = U) \<and> ?TOP \<inter> U = \<Inter>\<U>"
+      if \<U>: "\<U> \<subseteq> Collect ?\<Omega>" and "finite' \<U>" "A = \<Inter>\<U>" "\<U> \<noteq> {}" for \<U>
+    proof -
+      have "\<forall>U \<in> \<U>. \<exists>Y. U = Pi\<^sub>E I Y \<and> (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}"
+        using \<U> by auto
+      then obtain Y where Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = Pi\<^sub>E I (Y U) \<and> (\<forall>i. openin (X i) (Y U i)) \<and> finite {i. (Y U) i \<noteq> topspace (X i)}"
+        by metis
+      obtain U where "U \<in> \<U>"
+        using \<open>\<U> \<noteq> {}\<close> by blast
+      let ?F = "\<lambda>U. (\<lambda>i. {f. f i \<in> Y U i}) ` {i \<in> I. Y U i \<noteq> topspace (X i)}"
+      show ?thesis
+      proof (intro conjI exI)
+        show "finite (\<Union>U\<in>\<U>. ?F U)"
+          using Y \<open>finite' \<U>\<close> by auto
+        show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) = \<Inter>\<U>"
+        proof
+          have *: "f \<in> U"
+            if "U \<in> \<U>" and "\<forall>V\<in>\<U>. \<forall>i. i \<in> I \<and> Y V i \<noteq> topspace (X i) \<longrightarrow> f i \<in> Y V i"
+              and "\<forall>i\<in>I. f i \<in> topspace (X i)" and "f \<in> extensional I" for f U
+          proof -
+            have "Pi\<^sub>E I (Y U) = U"
+              using Y \<open>U \<in> \<U>\<close> by blast
+            then show "f \<in> U"
+              using that unfolding PiE_def Pi_def by blast
+          qed
+          show "?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U) \<subseteq> \<Inter>\<U>"
+            by (auto simp: PiE_iff *)
+          show "\<Inter>\<U> \<subseteq> ?TOP \<inter> \<Inter>(\<Union>U\<in>\<U>. ?F U)"
+            using Y openin_subset \<open>finite' \<U>\<close> by fastforce
+        qed
+      qed (use Y openin_subset in \<open>blast+\<close>)
+    qed
+    have 2: "\<exists>\<U>'. finite' \<U>' \<and> \<U>' \<subseteq> Collect ?\<Omega> \<and> \<Inter>\<U>' = ?TOP \<inter> \<Inter>\<U>"
+      if \<U>: "\<U> \<subseteq> Collect ?\<Psi>" and "finite \<U>" for \<U>
+    proof (cases "\<U>={}")
+      case True
+      then show ?thesis
+        apply (rule_tac x="{?TOP}" in exI, simp)
+        apply (rule_tac x="\<lambda>i. topspace (X i)" in exI)
+        apply force
+        done
+    next
+      case False
+      then obtain U where "U \<in> \<U>"
+        by blast
+      have "\<forall>U \<in> \<U>. \<exists>i Y. U = {f. f i \<in> Y} \<and> i \<in> I \<and> openin (X i) Y"
+        using \<U> by auto
+      then obtain J Y where
+        Y: "\<And>U. U \<in> \<U> \<Longrightarrow> U = {f. f (J U) \<in> Y U} \<and> J U \<in> I \<and> openin (X (J U)) (Y U)"
+        by metis
+      let ?G = "\<lambda>U. \<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)"
+      show ?thesis
+      proof (intro conjI exI)
+        show "finite (?G ` \<U>)" "?G ` \<U> \<noteq> {}"
+          using \<open>finite \<U>\<close> \<open>U \<in> \<U>\<close> by blast+
+        have *: "\<And>U. U \<in> \<U> \<Longrightarrow> openin (X (J U)) (Y U)"
+          using Y by force
+        show "?G ` \<U> \<subseteq> {Pi\<^sub>E I Y |Y. (\<forall>i. openin (X i) (Y i)) \<and> finite {i. Y i \<noteq> topspace (X i)}}"
+          apply clarsimp
+          apply (rule_tac x=" (\<lambda>i. if i = J U then Y U else topspace (X i))" in exI)
+          apply (auto simp: *)
+          done
+      next
+        show "(\<Inter>U\<in>\<U>. ?G U) = ?TOP \<inter> \<Inter>\<U>"
+        proof
+          have "(\<Pi>\<^sub>E i\<in>I. if i = J U then Y U else topspace (X i)) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (X i))"
+            apply (clarsimp simp: PiE_iff Ball_def all_conj_distrib split: if_split_asm)
+            using Y \<open>U \<in> \<U>\<close> openin_subset by blast+
+          then have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP"
+            using \<open>U \<in> \<U>\<close>
+            by fastforce
+          moreover have "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> \<Inter>\<U>"
+            using PiE_mem Y by fastforce
+          ultimately show "(\<Inter>U\<in>\<U>. ?G U) \<subseteq> ?TOP \<inter> \<Inter>\<U>"
+            by auto
+        qed (use Y in fastforce)
+      qed
+    qed
+    show ?thesis
+      unfolding relative_to_def intersection_of_def
+      by (safe; blast dest!: 1 2)
+  qed
+  show ?thesis
+    unfolding product_topology_def generate_topology_on_eq
+    apply (rule arg_cong [where f = topology])
+    apply (rule arg_cong [where f = "(union_of)arbitrary"])
+    apply (force simp: *)
+    done
+qed
+
+lemma%important topspace_product_topology:
   "topspace (product_topology T I) = (\<Pi>\<^sub>E i\<in>I. topspace(T i))"
 proof%unimportant
   show "topspace (product_topology T I) \<subseteq> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
-    unfolding product_topology_def apply (simp only: topology_generated_by_topspace)
+    unfolding product_topology_def topology_generated_by_topspace
     unfolding topspace_def by auto
   have "(\<Pi>\<^sub>E i\<in>I. topspace (T i)) \<in> {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
     using openin_topspace not_finite_existsD by auto
@@ -330,11 +563,11 @@
 lemma%unimportant product_topology_basis:
   assumes "\<And>i. openin (T i) (X i)" "finite {i. X i \<noteq> topspace (T i)}"
   shows "openin (product_topology T I) (\<Pi>\<^sub>E i\<in>I. X i)"
-unfolding product_topology_def apply (rule topology_generated_by_Basis) using assms by auto
+  unfolding product_topology_def
+  by (rule topology_generated_by_Basis) (use assms in auto)
 
 lemma%important product_topology_open_contains_basis:
-  assumes "openin (product_topology T I) U"
-          "x \<in> U"
+  assumes "openin (product_topology T I) U" "x \<in> U"
   shows "\<exists>X. x \<in> (\<Pi>\<^sub>E i\<in>I. X i) \<and> (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)} \<and> (\<Pi>\<^sub>E i\<in>I. X i) \<subseteq> U"
 proof%unimportant -
   have "generate_topology_on {(\<Pi>\<^sub>E i\<in>I. X i) |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}} U"
@@ -375,6 +608,114 @@
 qed
 
 
+lemma openin_product_topology:
+   "openin (product_topology X I) =
+    arbitrary union_of
+          ((finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)))
+           relative_to topspace (product_topology X I))"
+  apply (subst product_topology)
+  apply (simp add: topspace_product_topology topology_inverse' [OF istopology_subbase])
+  done
+
+lemma subtopology_PiE:
+  "subtopology (product_topology X I) (\<Pi>\<^sub>E i\<in>I. (S i)) = product_topology (\<lambda>i. subtopology (X i) (S i)) I"
+proof -
+  let ?P = "\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U"
+  let ?X = "\<Pi>\<^sub>E i\<in>I. topspace (X i)"
+  have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
+        finite intersection_of (?P relative_to ?X \<inter> Pi\<^sub>E I S) relative_to ?X \<inter> Pi\<^sub>E I S"
+    by (rule finite_intersection_of_relative_to)
+  also have "\<dots> = finite intersection_of
+                      ((\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
+                       relative_to ?X \<inter> Pi\<^sub>E I S)
+                   relative_to ?X \<inter> Pi\<^sub>E I S"
+    apply (rule arg_cong2 [where f = "(relative_to)"])
+     apply (rule arg_cong [where f = "(intersection_of)finite"])
+     apply (rule ext)
+     apply (auto simp: relative_to_def intersection_of_def)
+    done
+  finally
+  have "finite intersection_of ?P relative_to ?X \<inter> Pi\<^sub>E I S =
+        finite intersection_of
+          (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> (openin (X i) relative_to S i) U)
+          relative_to ?X \<inter> Pi\<^sub>E I S"
+    by (metis finite_intersection_of_relative_to)
+  then show ?thesis
+  unfolding topology_eq
+  apply clarify
+  apply (simp add: openin_product_topology flip: openin_relative_to)
+  apply (simp add: arbitrary_union_of_relative_to topspace_product_topology topspace_subtopology flip: PiE_Int)
+  done
+qed
+
+
+lemma product_topology_base_alt:
+   "finite intersection_of (\<lambda>F. (\<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U))
+    relative_to topspace(product_topology X I) =
+    (\<lambda>F. (\<exists>U. F =  Pi\<^sub>E I U \<and> finite {i \<in> I. U i \<noteq> topspace(X i)} \<and> (\<forall>i \<in> I. openin (X i) (U i))))"
+   (is "?lhs = ?rhs")
+proof -
+  have "(\<forall>F. ?lhs F \<longrightarrow> ?rhs F)"
+    unfolding all_relative_to all_intersection_of topspace_product_topology
+  proof clarify
+    fix \<F>
+    assume "finite \<F>" and "\<F> \<subseteq> {{f. f i \<in> U} |i U. i \<in> I \<and> openin (X i) U}"
+    then show "\<exists>U. (\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U \<and>
+          finite {i \<in> I. U i \<noteq> topspace (X i)} \<and> (\<forall>i\<in>I. openin (X i) (U i))"
+    proof (induction)
+      case (insert F \<F>)
+      then obtain U where eq: "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>\<F> = Pi\<^sub>E I U"
+        and fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}"
+        and ope: "\<And>i. i \<in> I \<Longrightarrow> openin (X i) (U i)"
+        by auto
+      obtain i V where "F = {f. f i \<in> V}" "i \<in> I" "openin (X i) V"
+        using insert by auto
+      let ?U = "\<lambda>j. U j \<inter> (if j = i then V else topspace(X j))"
+      show ?case
+      proof (intro exI conjI)
+        show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> \<Inter>insert F \<F> = Pi\<^sub>E I ?U"
+        using eq  PiE_mem \<open>i \<in> I\<close>  by (auto simp: \<open>F = {f. f i \<in> V}\<close>) fastforce
+      next
+        show "finite {i \<in> I. ?U i \<noteq> topspace (X i)}"
+          by (rule rev_finite_subset [OF finite.insertI [OF fin]]) auto
+      next
+        show "\<forall>i\<in>I. openin (X i) (?U i)"
+          by (simp add: \<open>openin (X i) V\<close> ope openin_Int)
+      qed
+    qed (auto intro: dest: not_finite_existsD)
+  qed
+  moreover have "(\<forall>F. ?rhs F \<longrightarrow> ?lhs F)"
+  proof clarify
+    fix U :: "'a \<Rightarrow> 'b set"
+    assume fin: "finite {i \<in> I. U i \<noteq> topspace (X i)}" and ope: "\<forall>i\<in>I. openin (X i) (U i)"
+    let ?U = "\<Inter>i\<in>{i \<in> I. U i \<noteq> topspace (X i)}. {x. x i \<in> U i}"
+    show "?lhs (Pi\<^sub>E I U)"
+      unfolding relative_to_def topspace_product_topology
+    proof (intro exI conjI)
+      show "(finite intersection_of (\<lambda>F. \<exists>i U. F = {f. f i \<in> U} \<and> i \<in> I \<and> openin (X i) U)) ?U"
+        using fin ope by (intro finite_intersection_of_Inter finite_intersection_of_inc) auto
+      show "(\<Pi>\<^sub>E i\<in>I. topspace (X i)) \<inter> ?U = Pi\<^sub>E I U"
+        using ope openin_subset by fastforce
+    qed
+  qed
+  ultimately show ?thesis
+    by meson
+qed
+
+
+lemma topspace_product_topology_alt:
+   "topspace (product_topology Y I) = {f \<in> extensional I. \<forall>k \<in> I. f k \<in> topspace(Y k)}"
+  by (force simp: product_topology PiE_def)
+
+lemma openin_product_topology_alt:
+  "openin (product_topology X I) S \<longleftrightarrow>
+    (\<forall>x \<in> S. \<exists>U. finite {i \<in> I. U i \<noteq> topspace(X i)} \<and>
+                 (\<forall>i \<in> I. openin (X i) (U i)) \<and> x \<in> Pi\<^sub>E I U \<and> Pi\<^sub>E I U \<subseteq> S)"
+  apply (simp add: openin_product_topology arbitrary_union_of_alt product_topology_base_alt, auto)
+  apply (drule bspec; blast)
+  done
+
+
 text \<open>The basic property of the product topology is the continuity of projections:\<close>
 
 lemma%unimportant continuous_on_topo_product_coordinates [simp]:
@@ -396,7 +737,7 @@
       using ** by auto
   }
   then show ?thesis unfolding continuous_on_topo_def
-    by (auto simp add: assms product_topology_topspace PiE_iff)
+    by (auto simp add: assms topspace_product_topology PiE_iff)
 qed
 
 lemma%important continuous_on_topo_coordinatewise_then_product [intro]:
@@ -427,7 +768,7 @@
   show "f `topspace T1 \<subseteq> \<Union>{Pi\<^sub>E I X |X. (\<forall>i. openin (T i) (X i)) \<and> finite {i. X i \<noteq> topspace (T i)}}"
     apply (subst topology_generated_by_topspace[symmetric])
     apply (subst product_topology_def[symmetric])
-    apply (simp only: product_topology_topspace)
+    apply (simp only: topspace_product_topology)
     apply (auto simp add: PiE_iff)
     using assms unfolding continuous_on_topo_def by auto
 qed
@@ -449,7 +790,7 @@
   have "f x \<in> topspace (product_topology T I)"
     using assms \<open>x \<in> topspace T1\<close> unfolding continuous_on_topo_def by auto
   then have "f x \<in> (\<Pi>\<^sub>E i\<in>I. topspace (T i))"
-    using product_topology_topspace by metis
+    using topspace_product_topology by metis
   then show "f x i = undefined"
     using \<open>i \<notin> I\<close> by (auto simp add: PiE_iff extensional_def)
 qed
@@ -479,7 +820,7 @@
 
 instance proof%unimportant
   have "topspace (product_topology (\<lambda>(i::'a). euclidean::('b topology)) UNIV) = UNIV"
-    unfolding product_topology_topspace topspace_euclidean by auto
+    unfolding topspace_product_topology topspace_euclidean by auto
   then show "open (UNIV::('a \<Rightarrow> 'b) set)"
     unfolding open_fun_def by (metis openin_topspace)
 qed (auto simp add: open_fun_def)
@@ -1233,6 +1574,8 @@
 by standard
 
 
+
+
 subsection%important \<open>Measurability\<close> (*FIX ME mv *)
 
 text \<open>There are two natural sigma-algebras on a product space: the borel sigma algebra,
diff -r c9ea9290880f -r 697789794af1 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Sep 24 14:33:17 2018 +0100
@@ -11,6 +11,7 @@
   "HOL-Library.Indicator_Function"
   "HOL-Library.Countable_Set"
   "HOL-Library.FuncSet"
+  "HOL-Library.Set_Idioms"
   Linear_Algebra
   Norm_Arith
 begin
@@ -817,6 +818,9 @@
   unfolding subtopology_def topology_inverse'[OF istopology_subtopology]
   by auto
 
+lemma openin_relative_to: "(openin X relative_to S) = openin (subtopology X S)"
+  by (force simp: relative_to_def openin_subtopology)
+
 lemma topspace_subtopology: "topspace (subtopology U V) = topspace U \<inter> V"
   by (auto simp: topspace_def openin_subtopology)
 
diff -r c9ea9290880f -r 697789794af1 src/HOL/Data_Structures/Sorting.thy
--- a/src/HOL/Data_Structures/Sorting.thy	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Data_Structures/Sorting.thy	Mon Sep 24 14:33:17 2018 +0100
@@ -270,7 +270,7 @@
 subsubsection "Functional Correctness"
 
 lemma mset_merge_adj:
-  "\<Union># image_mset mset (mset (merge_adj xss)) = \<Union># image_mset mset (mset xss)"
+  "\<Union># (image_mset mset (mset (merge_adj xss))) = \<Union># (image_mset mset (mset xss))"
 by(induction xss rule: merge_adj.induct) (auto simp: mset_merge)
 
 lemma mset_merge_all:
diff -r c9ea9290880f -r 697789794af1 src/HOL/Data_Structures/Tree234_Map.thy
--- a/src/HOL/Data_Structures/Tree234_Map.thy	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Data_Structures/Tree234_Map.thy	Mon Sep 24 14:33:17 2018 +0100
@@ -66,7 +66,7 @@
    GT \<Rightarrow> (case cmp x (fst ab3) of
             LT \<Rightarrow> (case upd x y t3 of
                     T\<^sub>i t3' \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3' ab3 t4)
-                  | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2(*q*) (Node3 t31 q t32 ab3 t4)) |
+                  | Up\<^sub>i t31 q t32 => Up\<^sub>i (Node2 t1 ab1 t2) ab2\<^cancel>\<open>q\<close> (Node3 t31 q t32 ab3 t4)) |
             EQ \<Rightarrow> T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 (x,y) t4) |
             GT \<Rightarrow> (case upd x y t4 of
                     T\<^sub>i t4' => T\<^sub>i (Node4 t1 ab1 t2 ab2 t3 ab3 t4')
diff -r c9ea9290880f -r 697789794af1 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/GCD.thy	Mon Sep 24 14:33:17 2018 +0100
@@ -1092,14 +1092,14 @@
 
 sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
 defines
-  Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
+  Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n") = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
 
 abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
   where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
 
 sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
 defines
-  Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Lcm_fin.F ..
+  Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n") = Lcm_fin.F ..
 
 abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
   where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
diff -r c9ea9290880f -r 697789794af1 src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Mon Sep 24 14:33:17 2018 +0100
@@ -161,7 +161,7 @@
 end
 
 lemma Sup_image_mono_le:
-  fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or> _" [900] 900)
+  fixes le_b (infix "\<sqsubseteq>" 60) and Sup_b ("\<Or>")
   assumes ccpo: "class.ccpo Sup_b (\<sqsubseteq>) lt_b"
   assumes chain: "Complete_Partial_Order.chain (\<sqsubseteq>) Y"
   and mono: "\<And>x y. \<lbrakk> x \<sqsubseteq> y; x \<in> Y \<rbrakk> \<Longrightarrow> f x \<le> f y"
@@ -556,7 +556,7 @@
 
 context
   fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix "\<sqsubseteq>" 60) 
-  and lub :: "'b set \<Rightarrow> 'b" ("\<Or> _" [900] 900)
+  and lub :: "'b set \<Rightarrow> 'b" ("\<Or>")
 begin
 
 lemma cont_fun_lub_Sup:
@@ -677,7 +677,7 @@
 by(rule monotoneI)(auto intro: bot intro: mono order_trans)
 
 lemma (in ccpo) mcont_if_bot:
-  fixes bot and lub ("\<Or> _" [900] 900) and ord (infix "\<sqsubseteq>" 60)
+  fixes bot and lub ("\<Or>") and ord (infix "\<sqsubseteq>" 60)
   assumes ccpo: "class.ccpo lub (\<sqsubseteq>) lt"
   and mono: "\<And>x y. \<lbrakk> x \<le> y; \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y"
   and cont: "\<And>Y. \<lbrakk> Complete_Partial_Order.chain (\<le>) Y; Y \<noteq> {}; \<And>x. x \<in> Y \<Longrightarrow> \<not> x \<le> bound \<rbrakk> \<Longrightarrow> f (\<Squnion>Y) = \<Or>(f ` Y)"
@@ -877,7 +877,7 @@
 end
 
 lemma admissible_leI:
-  fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or> _" [900] 900)
+  fixes ord (infix "\<sqsubseteq>" 60) and lub ("\<Or>")
   assumes "class.ccpo lub (\<sqsubseteq>) (mk_less (\<sqsubseteq>))"
   and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. f x)"
   and "mcont luba orda lub (\<sqsubseteq>) (\<lambda>x. g x)"
diff -r c9ea9290880f -r 697789794af1 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Sep 24 14:33:17 2018 +0100
@@ -2385,7 +2385,7 @@
   shows \<open>(\<Sum>x\<in>#A. y) = of_nat (size A) * y\<close>
   by (induction A) (auto simp: algebra_simps)
 
-abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union># _" [900] 900)
+abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#")
   where "\<Union># MM \<equiv> sum_mset MM" \<comment> \<open>FIXME ambiguous notation --
     could likewise refer to \<open>\<Squnion>#\<close>\<close>
 
diff -r c9ea9290880f -r 697789794af1 src/HOL/Mirabelle/ex/Ex.thy
--- a/src/HOL/Mirabelle/ex/Ex.thy	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/HOL/Mirabelle/ex/Ex.thy	Mon Sep 24 14:33:17 2018 +0100
@@ -3,7 +3,7 @@
 
 ML \<open>
   val rc = Isabelle_System.bash
-    "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; isabelle mirabelle arith Inner_Product.thy";
+    "cd \"$ISABELLE_HOME/src/HOL/Analysis\"; if isabelle build -n \"$MIRABELLE_LOGIC\"; then isabelle mirabelle arith Inner_Product.thy; fi";
   if rc <> 0 then error ("Mirabelle example failed: " ^ string_of_int rc)
   else ();
 \<close> \<comment> \<open>some arbitrary small test case\<close>
diff -r c9ea9290880f -r 697789794af1 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Sep 24 14:33:17 2018 +0100
@@ -56,13 +56,6 @@
   val specification_of: theory -> string -> term option * term list
   val hyp_spec_of: theory -> string -> Element.context_i list
 
-  type content =
-   {type_params: (string * sort) list,
-    params: ((string * typ) * mixfix) list,
-    asm: term option,
-    defs: term list}
-  val dest_locales: theory -> (string * content) list
-
   (* Storing results *)
   val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
   val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
@@ -93,6 +86,7 @@
   val add_dependency: string -> registration -> theory -> theory
 
   (* Diagnostic *)
+  val get_locales: theory -> string list
   val print_locales: bool -> theory -> unit
   val print_locale: theory -> bool -> xstring * Position.T -> unit
   val print_registrations: Proof.context -> xstring * Position.T -> unit
@@ -215,19 +209,6 @@
   Locales.map o Name_Space.map_table_entry name o map_locale o apsnd;
 
 
-(* content *)
-
-type content =
- {type_params: (string * sort) list,
-  params: ((string * typ) * mixfix) list,
-  asm: term option,
-  defs: term list};
-
-fun dest_locales thy =
-  (Locales.get thy, []) |-> Name_Space.fold_table
-    (fn (name, Loc {parameters = (type_params, params), spec = (asm, defs), ...}) =>
-      cons (name, {type_params = type_params, params = params, asm = asm, defs = defs}));
-
 
 (** Primitive operations **)
 
@@ -715,6 +696,8 @@
 
 (*** diagnostic commands and interfaces ***)
 
+fun get_locales thy = map #1 (Name_Space.dest_table (Locales.get thy));
+
 fun print_locales verbose thy =
   Pretty.block
     (Pretty.breaks
diff -r c9ea9290880f -r 697789794af1 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Sep 24 14:33:17 2018 +0100
@@ -415,24 +415,11 @@
 
 local
 
-fun goalN i = "goal" ^ string_of_int i;
-fun goals st = map goalN (1 upto Thm.nprems_of st);
-
-fun no_goal_cases st = map (rpair NONE) (goals st);
-
-fun goal_cases ctxt st =
-  Rule_Cases.make_common ctxt (Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
-
 fun apply_method text ctxt state =
   find_goal state |> (fn (goal_ctxt, {statement, using, goal, before_qed, after_qed}) =>
     Method.evaluate text ctxt using (goal_ctxt, goal)
     |> Seq.map_result (fn (goal_ctxt', goal') =>
-      let
-        val goal_ctxt'' = goal_ctxt'
-          |> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal');
-        val state' = state
-          |> map_goal (K (goal_ctxt'', statement, using, goal', before_qed, after_qed));
-      in state' end));
+        state |> map_goal (K (goal_ctxt', statement, using, goal', before_qed, after_qed))));
 
 in
 
diff -r c9ea9290880f -r 697789794af1 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Sep 24 14:33:17 2018 +0100
@@ -151,9 +151,8 @@
   val add_assms_cmd: Assumption.export ->
     (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
-  val dest_cases: Proof.context option -> Proof.context -> (string * (Rule_Cases.T * {legacy: bool})) list
+  val dest_cases: Proof.context option -> Proof.context -> (string * Rule_Cases.T) list
   val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
-  val update_cases_legacy: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
   val check_case: Proof.context -> bool ->
     string * Position.T -> binding option list -> Rule_Cases.T
@@ -228,7 +227,7 @@
 
 (** Isar proof context information **)
 
-type cases = (Rule_Cases.T * {legacy: bool}) Name_Space.table;
+type cases = Rule_Cases.T Name_Space.table;
 val empty_cases: cases = Name_Space.empty_table Markup.caseN;
 
 datatype data =
@@ -238,7 +237,7 @@
     tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
     consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
     facts: Facts.T,              (*local facts, based on initial global facts*)
-    cases: cases};               (*named case contexts: case, legacy, running index*)
+    cases: cases};               (*named case contexts*)
 
 fun make_data (mode, syntax, tsig, consts, facts, cases) =
   Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
@@ -1319,17 +1318,10 @@
 fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
   | drop_schematic b = b;
 
-fun update_case _ _ ("", _) cases = cases
-  | update_case _ _ (name, NONE) cases = Name_Space.del_table name cases
-  | update_case context legacy (name, SOME c) cases =
-      let
-        val binding = Binding.name name |> legacy ? Binding.concealed;
-        val (_, cases') = Name_Space.define context false (binding, (c, {legacy = legacy})) cases;
-      in cases' end;
-
-fun update_cases' legacy args ctxt =
-  let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
-  in map_cases (fold (update_case context legacy) args) ctxt end;
+fun update_case _ ("", _) cases = cases
+  | update_case _ (name, NONE) cases = Name_Space.del_table name cases
+  | update_case context (name, SOME c) cases =
+      #2 (Name_Space.define context false (Binding.name name, c) cases);
 
 fun fix (b, T) ctxt =
   let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
@@ -1337,8 +1329,9 @@
 
 in
 
-val update_cases = update_cases' false;
-val update_cases_legacy = update_cases' true;
+fun update_cases args ctxt =
+  let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
+  in map_cases (fold (update_case context) args) ctxt end;
 
 fun case_result c ctxt =
   let
@@ -1356,13 +1349,8 @@
 
 fun check_case ctxt internal (name, pos) param_specs =
   let
-    val (_, (Rule_Cases.Case {fixes, assumes, binds, cases}, {legacy})) =
+    val (_, Rule_Cases.Case {fixes, assumes, binds, cases}) =
       Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
-    val _ =
-      if legacy then
-        legacy_feature ("Bad case " ^ quote name ^ Position.here pos ^
-          " -- use proof method \"goal_cases\" instead")
-      else ();
 
     val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs;
     fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
@@ -1537,10 +1525,9 @@
 
 fun pretty_cases ctxt =
   let
-    fun mk_case (_, (_, {legacy = true})) = NONE
-      | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, {legacy = false})) =
-          SOME (name, (fixes, case_result c ctxt));
-    val cases = dest_cases NONE ctxt |> map_filter mk_case;
+    val cases =
+      dest_cases NONE ctxt |> map (fn (name, c as Rule_Cases.Case {fixes, ...}) =>
+        (name, (fixes, case_result c ctxt)));
   in
     if null cases then []
     else [Pretty.big_list "cases:" (map pretty_case cases)]
@@ -1563,20 +1550,18 @@
     fun is_case x t =
       x = Rule_Cases.case_conclN andalso not (Term.exists_subterm Term.is_Var t);
 
-    fun print_proof (name, (Rule_Cases.Case {fixes, binds, ...}, {legacy})) =
-      if legacy then NONE
-      else
-        let
-          val concl =
-            if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
-            then Rule_Cases.case_conclN else Auto_Bind.thesisN;
-        in
-          SOME (cat_lines
-            ["  case " ^ print_case name (map (Binding.name_of o #1) fixes),
-             "  then show ?" ^ concl ^ " sorry"])
-        end;
+    fun print_proof (name, Rule_Cases.Case {fixes, binds, ...}) =
+      let
+        val concl =
+          if exists (fn ((x, _), SOME t) => is_case x t | _ => false) binds
+          then Rule_Cases.case_conclN else Auto_Bind.thesisN;
+      in
+        cat_lines
+          ["  case " ^ print_case name (map (Binding.name_of o #1) fixes),
+           "  then show ?" ^ concl ^ " sorry"]
+      end;
   in
-    (case map_filter print_proof (dest_cases (SOME ctxt0) ctxt) of
+    (case map print_proof (dest_cases (SOME ctxt0) ctxt) of
       [] => ""
     | proofs =>
         "Proof outline with cases:\n" ^
diff -r c9ea9290880f -r 697789794af1 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/PIDE/headless.scala	Mon Sep 24 14:33:17 2018 +0100
@@ -71,6 +71,12 @@
     val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
     val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
   {
+    def nodes_pending: List[(Document.Node.Name, Document_Status.Node_Status)] =
+    {
+      val committed = nodes_committed.iterator.map(_._1).toSet
+      nodes.filter(p => !committed(p._1))
+    }
+
     def snapshot(name: Document.Node.Name): Document.Snapshot =
       stable_snapshot(state, version, name)
 
@@ -136,31 +142,29 @@
           commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
         : Use_Theories_State =
       {
-        val st1 =
+        val already_committed1 =
           if (commit.isDefined) {
-            val already_committed1 =
-              (already_committed /: dep_theories)({ case (committed, name) =>
-                def parents_committed: Boolean =
-                  version.nodes(name).header.imports.forall({ case (parent, _) =>
-                    Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
-                  })
-                if (!committed.isDefinedAt(name) && parents_committed &&
-                    state.node_consolidated(version, name))
-                {
-                  val snapshot = stable_snapshot(state, version, name)
-                  val status = Document_Status.Node_Status.make(state, version, name)
-                  commit.get.apply(snapshot, status)
-                  committed + (name -> status)
-                }
-                else committed
-              })
-            copy(already_committed = already_committed1)
+            (already_committed /: dep_theories)({ case (committed, name) =>
+              def parents_committed: Boolean =
+                version.nodes(name).header.imports.forall({ case (parent, _) =>
+                  Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
+                })
+              if (!committed.isDefinedAt(name) && parents_committed &&
+                  state.node_consolidated(version, name))
+              {
+                val snapshot = stable_snapshot(state, version, name)
+                val status = Document_Status.Node_Status.make(state, version, name)
+                commit.get.apply(snapshot, status)
+                committed + (name -> status)
+              }
+              else committed
+            })
           }
-          else this
+          else already_committed
 
         if (beyond_limit || watchdog(watchdog_timeout) ||
           dep_theories.forall(name =>
-            already_committed.isDefinedAt(name) ||
+            already_committed1.isDefinedAt(name) ||
             state.node_consolidated(version, name) ||
             nodes_status.quasi_consolidated(name)))
         {
@@ -170,14 +174,14 @@
           val nodes_committed =
             for {
               name <- dep_theories
-              status <- already_committed.get(name)
+              status <- already_committed1.get(name)
             } yield (name -> status)
 
           try { result.fulfill(new Use_Theories_Result(state, version, nodes, nodes_committed)) }
           catch { case _: IllegalStateException => }
         }
 
-        st1
+        copy(already_committed = already_committed1)
       }
     }
 
diff -r c9ea9290880f -r 697789794af1 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Mon Sep 24 14:33:17 2018 +0100
@@ -22,7 +22,7 @@
   val is_tid: string -> bool
   datatype token_kind =
     Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
-    String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF
+    String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF
   eqtype token
   val kind_of_token: token -> token_kind
   val str_of_token: token -> string
@@ -120,13 +120,13 @@
 
 datatype token_kind =
   Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
-  String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF;
+  String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF;
 
 val token_kinds =
   Vector.fromList
    [Literal, Ident, Long_Ident, Var, Type_Ident, Type_Var, Num, Float, Str,
-    String, Cartouche, Space, Comment NONE, Comment (SOME Comment.Comment),
-    Comment (SOME Comment.Cancel), Comment (SOME Comment.Latex), Dummy, EOF];
+    String, Cartouche, Space, Comment Comment.Comment, Comment Comment.Cancel,
+    Comment Comment.Latex, Dummy, EOF];
 
 fun token_kind i = Vector.sub (token_kinds, i);
 fun token_kind_index k = #1 (the (Vector.findi (fn (_, k') => k = k') token_kinds));
@@ -301,8 +301,7 @@
 
     val scan =
       Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
-      Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) ||
-      Comment.scan >> (fn (kind, ss) => token (Comment (SOME kind)) ss) ||
+      Comment.scan >> (fn (kind, ss) => token (Comment kind) ss) ||
       Scan.max token_leq scan_lit scan_val ||
       scan_string >> token String ||
       scan_str >> token Str ||
diff -r c9ea9290880f -r 697789794af1 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Mon Sep 24 14:33:17 2018 +0100
@@ -341,12 +341,6 @@
 
     val toks = Syntax.tokenize syn raw syms;
     val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
-    val _ = toks |> List.app (fn tok =>
-      (case Lexicon.kind_of_token tok of
-        Lexicon.Comment NONE =>
-          legacy_feature ("Old-style inner comment: use \"\<comment> \<open>...\<close>\" or \"\<^cancel>\<open>...\<close>\" instead" ^
-            Position.here (Lexicon.pos_of_token tok))
-      | _ => ()));
 
     val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
       handle ERROR msg =>
diff -r c9ea9290880f -r 697789794af1 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Thy/export_theory.ML	Mon Sep 24 14:33:17 2018 +0100
@@ -70,23 +70,29 @@
   (fold_types o fold_atyps) (fn TFree (a, S) => is_free used a ? insert (op =) (a, S) | _ => I);
 
 
-(* locale support *)
+(* locale content *)
 
-fun locale_axioms thy loc =
+fun locale_content thy loc =
   let
-    val (intro1, intro2) = Locale.intros_of thy loc;
-    fun intros_tac ctxt = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2);
-    val res =
-      Proof_Context.init_global thy
-      |> Interpretation.interpretation ([(loc, (("", false), (Expression.Named [], [])))], [])
-      |> Proof.refine (Method.Basic (METHOD o intros_tac))
-      |> Seq.filter_results
-      |> try Seq.hd;
-  in
-    (case res of
-      SOME st => Thm.prems_of (#goal (Proof.goal st))
-    | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
-  end;
+    val args = map #1 (Locale.params_of thy loc);
+    val axioms =
+      let
+        val (intro1, intro2) = Locale.intros_of thy loc;
+        fun intros_tac ctxt = Method.try_intros_tac ctxt (the_list intro1 @ the_list intro2);
+        val inst = Expression.Named (args |> map (fn (x, T) => (x, Free (x, T))));
+        val res =
+          Proof_Context.init_global thy
+          |> Interpretation.interpretation ([(loc, (("", false), (inst, [])))], [])
+          |> Proof.refine (Method.Basic (METHOD o intros_tac))
+          |> Seq.filter_results
+          |> try Seq.hd;
+      in
+        (case res of
+          SOME st => Thm.prems_of (#goal (Proof.goal st))
+        | NONE => raise Fail ("Cannot unfold locale " ^ quote loc))
+      end;
+    val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) []);
+  in {typargs = typargs, args = args, axioms = axioms} end;
 
 
 (* general setup *)
@@ -272,17 +278,19 @@
       let open XML.Encode Term_XML.Encode
       in triple (list (pair string sort)) (list (pair string typ)) (list (encode_axiom used)) end;
 
-    fun export_locale loc ({type_params, params, ...}: Locale.content) =
+    fun export_locale loc =
       let
-        val axioms = locale_axioms thy loc;
-        val args = map #1 params;
-        val typargs = rev (fold Term.add_tfrees (map Free args @ axioms) (rev type_params));
+        val {typargs, args, axioms} = locale_content thy loc;
         val used = fold Name.declare (map #1 typargs @ map #1 args) Name.context;
-      in encode_locale used (typargs, args, axioms) end;
+      in encode_locale used (typargs, args, axioms) end
+      handle ERROR msg =>
+        cat_error msg ("The error(s) above occurred in locale " ^
+          quote (Locale.markup_name thy_ctxt loc));
 
     val _ =
-      export_entities "locales" (SOME oo export_locale) Locale.locale_space
-        (Locale.dest_locales thy);
+      export_entities "locales" (fn loc => fn () => SOME (export_locale loc))
+        Locale.locale_space
+        (map (rpair ()) (Locale.get_locales thy));
 
 
     (* parents *)
diff -r c9ea9290880f -r 697789794af1 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Thy/present.scala	Mon Sep 24 14:33:17 2018 +0100
@@ -319,6 +319,6 @@
       build_document(document_dir = document_dir, document_name = document_name,
         document_format = document_format, tags = tags)
     }
-    catch { case ERROR(msg) => Output.writeln(msg); sys.exit(1) }
+    catch { case ERROR(msg) => Output.writeln(msg); sys.exit(2) }
   })
 }
diff -r c9ea9290880f -r 697789794af1 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Sep 24 14:33:17 2018 +0100
@@ -196,21 +196,31 @@
     def imported_sources(name: String): List[SHA1.Digest] =
       session_bases(name).imported_sources.map(_._2)
 
-    def used_theories_condition(warning: String => Unit = _ => ()): List[Document.Node.Name] =
+    def used_theories_condition(default_options: Options, warning: String => Unit = _ => ())
+      : List[(Options, Document.Node.Name)] =
+    {
+      val default_skip_proofs = default_options.bool("skip_proofs")
       for {
         session_name <- sessions_structure.build_topological_order
         (options, name) <- session_bases(session_name).used_theories
         if {
+          def warn(msg: String): Unit = warning("Skipping theory " + name + "  (" + msg + ")")
+
           val conditions =
             space_explode(',', options.string("condition")).
               filter(cond => Isabelle_System.getenv(cond) == "")
-          if (conditions.isEmpty) true
-          else {
-            warning("Skipping theory " + name + "  (condition " + conditions.mkString(" ") + ")")
+          if (conditions.nonEmpty) {
+            warn("condition " + conditions.mkString(" "))
             false
           }
+          else if (default_skip_proofs && !options.bool("skip_proofs")) {
+            warn("option skip_proofs")
+            false
+          }
+          else true
         }
-      } yield name
+      } yield (options, name)
+    }
 
     def sources(name: String): List[SHA1.Digest] =
       session_bases(name).sources.map(_._2)
diff -r c9ea9290880f -r 697789794af1 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Mon Sep 24 14:33:17 2018 +0100
@@ -95,7 +95,7 @@
     commit_cleanup_delay: Time = Headless.default_commit_cleanup_delay,
     watchdog_timeout: Time = Headless.default_watchdog_timeout,
     system_mode: Boolean = false,
-    selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
+    selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
   {
     if (Build.build_logic(options, logic, build_heap = true, progress = progress,
       dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
@@ -112,7 +112,9 @@
     val include_sessions =
       deps.sessions_structure.imports_topological_order
 
-    val use_theories = deps.used_theories_condition(progress.echo_warning).map(_.theory)
+    val use_theories =
+      for { (_, name) <- deps.used_theories_condition(dump_options, progress.echo_warning) }
+      yield name.theory
 
 
     /* dump aspects asynchronously */
@@ -165,12 +167,16 @@
         commit_cleanup_delay = commit_cleanup_delay,
         watchdog_timeout = watchdog_timeout)
 
-    val session_result = session.stop()
+    session.stop()
 
     val consumer_ok = Consumer.shutdown()
 
-    if (use_theories_result.ok && consumer_ok) session_result
-    else session_result.error_rc
+    use_theories_result.nodes_pending match {
+      case Nil =>
+      case pending => error("Pending theories " + commas_quote(pending.map(p => p._1.toString)))
+    }
+
+    use_theories_result.ok && consumer_ok
   }
 
 
@@ -243,7 +249,7 @@
 
       val progress = new Console_Progress(verbose = verbose)
 
-      val result =
+      val ok =
         progress.interrupt_handler {
           dump(options, logic,
             aspects = aspects,
@@ -264,8 +270,6 @@
               sessions = sessions))
         }
 
-      progress.echo(result.timing.message_resources)
-
-      sys.exit(result.rc)
+      if (!ok) sys.exit(2)
     })
 }
diff -r c9ea9290880f -r 697789794af1 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Pure/Tools/server.scala	Mon Sep 24 14:33:17 2018 +0100
@@ -485,7 +485,7 @@
       }
       else if (operation_exit) {
         val ok = Server.exit(name)
-        sys.exit(if (ok) 0 else 1)
+        sys.exit(if (ok) 0 else 2)
       }
       else {
         val log = Logger.make(log_file)
diff -r c9ea9290880f -r 697789794af1 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Sep 24 14:33:08 2018 +0100
+++ b/src/Tools/VSCode/src/server.scala	Mon Sep 24 14:33:17 2018 +0100
@@ -361,7 +361,7 @@
 
   def exit() {
     log("\n")
-    sys.exit(if (session_.value.isDefined) 1 else 0)
+    sys.exit(if (session_.value.isDefined) 2 else 0)
   }