Merged
authoreberlm <eberlm@in.tum.de>
Fri, 04 Aug 2017 18:03:50 +0200
changeset 66367 1f66c7d77002
parent 66317 56f8bfe1211c (current diff)
parent 66340 1a8441ec5ced (diff)
child 66369 a8b89392ecb6
Merged
--- a/Admin/components/components.sha1	Thu Aug 03 13:35:28 2017 +0200
+++ b/Admin/components/components.sha1	Fri Aug 04 18:03:50 2017 +0200
@@ -5,6 +5,7 @@
 e7ffe4238b61a3c1ee87aca4421e7a612e09b836  ci-extras-1.tar.gz
 70105fd6fbfd1a868383fc510772b95234325d31  csdp-6.x.tar.gz
 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7  cvc3-2.4.1.tar.gz
+3682476dc5e915cf260764fa5b86f1ebdab57507  cvc4-1.5.tar.gz
 a5e02b5e990da4275dc5d4480c3b72fc73160c28  cvc4-1.5pre-1.tar.gz
 4d9658fd2688ae8ac78da8fdfcbf85960f871b71  cvc4-1.5pre-2.tar.gz
 b01fdb93f2dc2b8bcfd41c6091d91b37d6e240f9  cvc4-1.5pre-3.tar.gz
--- a/Admin/components/main	Thu Aug 03 13:35:28 2017 +0200
+++ b/Admin/components/main	Fri Aug 04 18:03:50 2017 +0200
@@ -1,7 +1,7 @@
 #main components for everyday use, without big impact on overall build time
 bash_process-1.2.1
 csdp-6.x
-cvc4-1.5pre-4
+cvc4-1.5
 e-1.8
 isabelle_fonts-20160830
 jdk-8u131
--- a/src/Doc/Implementation/Local_Theory.thy	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy	Fri Aug 04 18:03:50 2017 +0200
@@ -91,8 +91,7 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
-  @{index_ML Named_Target.init: "(local_theory -> local_theory) option ->
-    string -> theory -> local_theory"} \\[1ex]
+  @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
   @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory"} \\
   @{index_ML Local_Theory.note: "Attrib.binding * thm list ->
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Aug 04 18:03:50 2017 +0200
@@ -7,6 +7,24 @@
   imports Lebesgue_Measure Henstock_Kurzweil_Integration Complete_Measure Set_Integral
 begin
 
+lemma finite_product_dependent: (*FIXME DELETE*)
+  assumes "finite s"
+    and "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
+  shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
+  using assms
+proof induct
+  case (insert x s)
+  have *: "{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} =
+    (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
+  show ?case
+    unfolding *
+    apply (rule finite_UnI)
+    using insert
+    apply auto
+    done
+qed auto
+
+
 lemma le_left_mono: "x \<le> y \<Longrightarrow> y \<le> a \<longrightarrow> x \<le> (a::'a::preorder)"
   by (auto intro: order_trans)
 
@@ -1633,11 +1651,16 @@
       then show "\<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
         by force
     qed
-    from choice[OF this] guess k .. note k=conjunctD2[OF this[rule_format],rule_format]
-
+    then obtain k where k: "\<And>x. 0 < k x"
+                       "\<And>i x. \<lbrakk>i \<in> d; x \<notin> i\<rbrakk> \<Longrightarrow> ball x (k x) \<inter> i = {}"
+      by metis
     have "e/2 > 0"
       using e by auto
-    from henstock_lemma[OF assms(1) this] guess g . note g=this[rule_format]
+    from henstock_lemma[OF assms(1) this] 
+    obtain g where g: "gauge g"
+          "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; g fine p\<rbrakk> 
+                \<Longrightarrow> (\<Sum>(x, k)\<in>p. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
+      by (metis (no_types, lifting))      
     let ?g = "\<lambda>x. g x \<inter> ball x (k x)"
     show ?case
       apply (rule_tac x="?g" in exI)
@@ -1716,15 +1739,12 @@
           assume y: "y \<in> cbox a b"
           then have "\<exists>x l. (x, l) \<in> p \<and> y\<in>l"
             unfolding p'(6)[symmetric] by auto
-          then guess x l by (elim exE) note xl=conjunctD2[OF this]
+          then obtain x l where xl: "(x, l) \<in> p" "y \<in> l" by metis
           then have "\<exists>k. k \<in> d \<and> y \<in> k"
             using y unfolding d'(6)[symmetric] by auto
-          then guess i .. note i = conjunctD2[OF this]
+          then obtain i where i: "i \<in> d" "y \<in> i" by metis
           have "x \<in> i"
-            using fineD[OF p(3) xl(1)]
-            using k(2)[OF i(1), of x]
-            using i(2) xl(2)
-            by auto
+            using fineD[OF p(3) xl(1)] using k(2) i xl by auto
           then show "y \<in> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
             unfolding p'_def Union_iff
             apply (rule_tac x="i \<inter> l" in bexI)
@@ -1735,12 +1755,7 @@
       qed
 
       then have "(\<Sum>(x, k)\<in>p'. norm (content k *\<^sub>R f x - integral k f)) < e / 2"
-        apply -
-        apply (rule g(2)[rule_format])
-        unfolding tagged_division_of_def
-        apply safe
-        apply (rule gp')
-        done
+        using g(2) gp' tagged_division_of_def by blast
       then have **: "\<bar>(\<Sum>(x,k)\<in>p'. norm (content k *\<^sub>R f x)) - (\<Sum>(x,k)\<in>p'. norm (integral k f))\<bar> < e / 2"
         unfolding split_def
         using p''
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Fri Aug 04 18:03:50 2017 +0200
@@ -12,6 +12,7 @@
 imports Interval_Integral
 begin
 
+
 lemma nn_integral_substitution_aux:
   fixes f :: "real \<Rightarrow> ennreal"
   assumes Mf: "f \<in> borel_measurable borel"
--- a/src/HOL/Analysis/Tagged_Division.thy	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/HOL/Analysis/Tagged_Division.thy	Fri Aug 04 18:03:50 2017 +0200
@@ -10,23 +10,6 @@
   Topology_Euclidean_Space
 begin
 
-lemma finite_product_dependent: (*FIXME DELETE*)
-  assumes "finite s"
-    and "\<And>x. x \<in> s \<Longrightarrow> finite (t x)"
-  shows "finite {(i, j) |i j. i \<in> s \<and> j \<in> t i}"
-  using assms
-proof induct
-  case (insert x s)
-  have *: "{(i, j) |i j. i \<in> insert x s \<and> j \<in> t i} =
-    (\<lambda>y. (x,y)) ` (t x) \<union> {(i, j) |i j. i \<in> s \<and> j \<in> t i}" by auto
-  show ?case
-    unfolding *
-    apply (rule finite_UnI)
-    using insert
-    apply auto
-    done
-qed auto
-
 lemma sum_Sigma_product:
   assumes "finite S"
     and "\<And>i. i \<in> S \<Longrightarrow> finite (T i)"
@@ -210,18 +193,18 @@
 
 subsection \<open>The notion of a gauge --- simply an open set containing the point.\<close>
 
-definition "gauge d \<longleftrightarrow> (\<forall>x. x \<in> d x \<and> open (d x))"
+definition "gauge \<gamma> \<longleftrightarrow> (\<forall>x. x \<in> \<gamma> x \<and> open (\<gamma> x))"
 
 lemma gaugeI:
-  assumes "\<And>x. x \<in> g x"
-    and "\<And>x. open (g x)"
-  shows "gauge g"
+  assumes "\<And>x. x \<in> \<gamma> x"
+    and "\<And>x. open (\<gamma> x)"
+  shows "gauge \<gamma>"
   using assms unfolding gauge_def by auto
 
 lemma gaugeD[dest]:
-  assumes "gauge d"
-  shows "x \<in> d x"
-    and "open (d x)"
+  assumes "gauge \<gamma>"
+  shows "x \<in> \<gamma> x"
+    and "open (\<gamma> x)"
   using assms unfolding gauge_def by auto
 
 lemma gauge_ball_dependent: "\<forall>x. 0 < e x \<Longrightarrow> gauge (\<lambda>x. ball x (e x))"
@@ -233,7 +216,7 @@
 lemma gauge_trivial[intro!]: "gauge (\<lambda>x. ball x 1)"
   by (rule gauge_ball) auto
 
-lemma gauge_Int[intro]: "gauge d1 \<Longrightarrow> gauge d2 \<Longrightarrow> gauge (\<lambda>x. d1 x \<inter> d2 x)"
+lemma gauge_Int[intro]: "gauge \<gamma>1 \<Longrightarrow> gauge \<gamma>2 \<Longrightarrow> gauge (\<lambda>x. \<gamma>1 x \<inter> \<gamma>2 x)"
   unfolding gauge_def by auto
 
 lemma gauge_reflect:
@@ -244,10 +227,10 @@
 
 lemma gauge_Inter:
   assumes "finite S"
-    and "\<And>d. d\<in>S \<Longrightarrow> gauge (f d)"
-  shows "gauge (\<lambda>x. \<Inter>{f d x | d. d \<in> S})"
+    and "\<And>u. u\<in>S \<Longrightarrow> gauge (f u)"
+  shows "gauge (\<lambda>x. \<Inter>{f u x | u. u \<in> S})"
 proof -
-  have *: "\<And>x. {f d x |d. d \<in> S} = (\<lambda>d. f d x) ` S"
+  have *: "\<And>x. {f u x |u. u \<in> S} = (\<lambda>u. f u x) ` S"
     by auto
   show ?thesis
     unfolding gauge_def unfolding *
@@ -314,18 +297,15 @@
     assume "s = {{a}}" "K\<in>s"
     then have "\<exists>x y. K = cbox x y"
       apply (rule_tac x=a in exI)+
-      apply (force simp: cbox_sing)
+      apply force
       done
   }
   ultimately show ?l
     unfolding division_of_def cbox_sing by auto
 next
   assume ?l
-  {
-    fix x
-    assume x: "x \<in> s" have "x = {a}"
-      by (metis \<open>s division_of cbox a a\<close> cbox_sing division_ofD(2) division_ofD(3) subset_singletonD x)
-  }
+  have "x = {a}" if  "x \<in> s" for x
+    by (metis \<open>s division_of cbox a a\<close> cbox_sing division_ofD(2) division_ofD(3) subset_singletonD that)
   moreover have "s \<noteq> {}"
     using \<open>s division_of cbox a a\<close> by auto
   ultimately show ?r
@@ -401,11 +381,8 @@
     have *: "\<And>s. \<Union>{x\<in>s. x \<noteq> {}} = \<Union>s"
       by auto
     show "\<Union>?A = s1 \<inter> s2"
-      apply (rule set_eqI)
-      unfolding * and UN_iff
-      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)]
-      apply auto
-      done
+      unfolding * 
+      using division_ofD(6)[OF assms(1)] and division_ofD(6)[OF assms(2)] by auto
     {
       fix k
       assume "k \<in> ?A"
@@ -461,14 +438,14 @@
     unfolding * by auto
 qed
 
-lemma elementary_inter:
+lemma elementary_Int:
   fixes s t :: "'a::euclidean_space set"
   assumes "p1 division_of s"
     and "p2 division_of t"
   shows "\<exists>p. p division_of (s \<inter> t)"
 using assms division_inter by blast
 
-lemma elementary_inters:
+lemma elementary_Inter:
   assumes "finite f"
     and "f \<noteq> {}"
     and "\<forall>s\<in>f. \<exists>p. p division_of (s::('a::euclidean_space) set)"
@@ -488,7 +465,7 @@
     moreover obtain px where "px division_of x"
       using insert(5)[rule_format,OF insertI1] ..
     ultimately show ?thesis
-      by (simp add: elementary_inter Inter_insert)
+      by (simp add: elementary_Int Inter_insert)
   qed
 qed auto
 
@@ -548,13 +525,9 @@
   show "cbox c d \<in> p"
     unfolding p_def
     by (auto simp add: box_eq_empty cbox_def intro!: image_eqI[where x="\<lambda>(i::'a)\<in>Basis. (c, d)"])
-  {
-    fix i :: 'a
-    assume "i \<in> Basis"
-    with incl nonempty have "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i"
-      unfolding box_eq_empty subset_box by (auto simp: not_le)
-  }
-  note ord = this
+  have ord: "a \<bullet> i \<le> c \<bullet> i" "c \<bullet> i \<le> d \<bullet> i" "d \<bullet> i \<le> b \<bullet> i" if "i \<in> Basis" for i
+    using incl nonempty that
+    unfolding box_eq_empty subset_box by (auto simp: not_le)
 
   show "p division_of (cbox a b)"
   proof (rule division_ofI)
@@ -665,8 +638,8 @@
   then have di: "\<And>x. x \<in> p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})"
     by (meson Diff_subset division_of_subset)
   have "\<exists>d. d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)"
-    apply (rule elementary_inters [OF finite_imageI[OF p(1)]])
-    apply (auto dest: di simp: False elementary_inters [OF finite_imageI[OF p(1)]])
+    apply (rule elementary_Inter [OF finite_imageI[OF p(1)]])
+    apply (auto dest: di simp: False elementary_Inter [OF finite_imageI[OF p(1)]])
     done
   then obtain d where d: "d division_of \<Inter>((\<lambda>i. \<Union>(q i - {i})) ` p)" ..
   have "d \<union> p division_of cbox a b"
@@ -719,12 +692,7 @@
   obtains p where "(insert (cbox a b) p) division_of (cbox a b \<union> cbox c d)"
 proof (cases "cbox c d = {}")
   case True
-  show ?thesis
-    apply (rule that[of "{}"])
-    unfolding True
-    using assms
-    apply auto
-    done
+  with assms that show ?thesis by force
 next
   case False
   show ?thesis
@@ -812,14 +780,13 @@
         by auto
       show "finite ?D"
         using "*" pdiv(1) q(1) by auto
-      have lem1: "\<And>f s. \<Union>\<Union>(f ` s) = \<Union>((\<lambda>x. \<Union>(f x)) ` s)"
-        by auto
-      have lem2: "\<And>f s. f \<noteq> {} \<Longrightarrow> \<Union>{s \<union> t |t. t \<in> f} = s \<union> \<Union>f"
+      have "\<Union>?D = (\<Union>x\<in>p. \<Union>insert (cbox a b) (q x))"
         by auto
-      show "\<Union>?D = cbox a b \<union> \<Union>p"
-        unfolding * lem1
-        unfolding lem2[OF \<open>p \<noteq> {}\<close>, of "cbox a b", symmetric]
-        using q(6)  by auto
+      also have "... = \<Union>{cbox a b \<union> t |t. t \<in> p}"
+        using q(6) by auto
+      also have "... = cbox a b \<union> \<Union>p"
+        using \<open>p \<noteq> {}\<close> by auto
+      finally show "\<Union>?D = cbox a b \<union> \<Union>p" .
       show "K \<subseteq> cbox a b \<union> \<Union>p" "K \<noteq> {}" if "K \<in> ?D" for K
         using q that by blast+
       show "\<exists>a b. K = cbox a b" if "K \<in> ?D" for K
@@ -920,7 +887,7 @@
       apply auto
     done
   then obtain r2 where r2: "r2 division_of (\<Union>(r1 - p)) \<inter> (\<Union>q)"
-    by (metis assms(2) divq(6) elementary_inter)
+    by (metis assms(2) divq(6) elementary_Int)
   {
     fix x
     assume x: "x \<in> T" "x \<notin> S"
@@ -1130,9 +1097,8 @@
   assumes "s tagged_partial_division_of i"
     and "t \<subseteq> s"
   shows "t tagged_partial_division_of i"
-  using assms
+  using assms finite_subset[OF assms(2)]
   unfolding tagged_partial_division_of_def
-  using finite_subset[OF assms(2)]
   by blast
 
 lemma tag_in_interval: "p tagged_division_of i \<Longrightarrow> (x, k) \<in> p \<Longrightarrow> x \<in> i"
@@ -1183,28 +1149,28 @@
 qed
 
 lemma tagged_division_unions:
-  assumes "finite iset"
-    and "\<forall>i\<in>iset. pfn i tagged_division_of i"
-    and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
-  shows "\<Union>(pfn ` iset) tagged_division_of (\<Union>iset)"
+  assumes "finite I"
+    and "\<forall>i\<in>I. pfn i tagged_division_of i"
+    and "\<forall>i1\<in>I. \<forall>i2\<in>I. i1 \<noteq> i2 \<longrightarrow> interior(i1) \<inter> interior(i2) = {}"
+  shows "\<Union>(pfn ` I) tagged_division_of (\<Union>I)"
 proof (rule tagged_division_ofI)
   note assm = tagged_division_ofD[OF assms(2)[rule_format]]
-  show "finite (\<Union>(pfn ` iset))"
+  show "finite (\<Union>(pfn ` I))"
     using assms by auto
-  have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` iset)"
+  have "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` I)} = \<Union>((\<lambda>i. \<Union>{k. \<exists>x. (x, k) \<in> pfn i}) ` I)"
     by blast
-  also have "\<dots> = \<Union>iset"
+  also have "\<dots> = \<Union>I"
     using assm(6) by auto
-  finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` iset)} = \<Union>iset" .
+  finally show "\<Union>{k. \<exists>x. (x, k) \<in> \<Union>(pfn ` I)} = \<Union>I" .
   fix x k
-  assume xk: "(x, k) \<in> \<Union>(pfn ` iset)"
-  then obtain i where i: "i \<in> iset" "(x, k) \<in> pfn i"
+  assume xk: "(x, k) \<in> \<Union>(pfn ` I)"
+  then obtain i where i: "i \<in> I" "(x, k) \<in> pfn i"
     by auto
-  show "x \<in> k" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>iset"
+  show "x \<in> k" "\<exists>a b. k = cbox a b" "k \<subseteq> \<Union>I"
     using assm(2-4)[OF i] using i(1) by auto
   fix x' k'
-  assume xk': "(x', k') \<in> \<Union>(pfn ` iset)" "(x, k) \<noteq> (x', k')"
-  then obtain i' where i': "i' \<in> iset" "(x', k') \<in> pfn i'"
+  assume xk': "(x', k') \<in> \<Union>(pfn ` I)" "(x, k) \<noteq> (x', k')"
+  then obtain i' where i': "i' \<in> I" "(x', k') \<in> pfn i'"
     by auto
   have *: "\<And>a b. i \<noteq> i' \<Longrightarrow> a \<subseteq> i \<Longrightarrow> b \<subseteq> i' \<Longrightarrow> interior a \<inter> interior b = {}"
     using i(1) i'(1)
@@ -1379,8 +1345,8 @@
 
 lemma division_points_psubset:
   fixes a :: "'a::euclidean_space"
-  assumes "d division_of (cbox a b)"
-      and "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
+  assumes d: "d division_of (cbox a b)"
+      and altb: "\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i"  "a\<bullet>k < c" "c < b\<bullet>k"
       and "l \<in> d"
       and disj: "interval_lowerbound l\<bullet>k = c \<or> interval_upperbound l\<bullet>k = c"
       and k: "k \<in> Basis"
@@ -1390,14 +1356,12 @@
          division_points (cbox a b) d" (is "?D2 \<subset> ?D")
 proof -
   have ab: "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i"
-    using assms(2) by (auto intro!:less_imp_le)
-  guess u v using division_ofD(4)[OF assms(1,5)] by (elim exE) note l=this
+    using altb by (auto intro!:less_imp_le)
+  obtain u v where l: "l = cbox u v"
+    using d \<open>l \<in> d\<close> by blast
   have uv: "\<forall>i\<in>Basis. u\<bullet>i \<le> v\<bullet>i" "\<forall>i\<in>Basis. a\<bullet>i \<le> u\<bullet>i \<and> v\<bullet>i \<le> b\<bullet>i"
-    using division_ofD(2,2,3)[OF assms(1,5)] unfolding l box_ne_empty
-    using subset_box(1)
-    apply auto
-    apply blast+
-    done
+    apply (metis assms(5) box_ne_empty(1) cbox_division_memE d l)
+    by (metis assms(5) box_ne_empty(1) cbox_division_memE d l subset_box(1))
   have *: "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_upperbound l \<bullet> k}) \<bullet> k = interval_upperbound l \<bullet> k"
           "interval_upperbound (cbox a b \<inter> {x. x \<bullet> k \<le> interval_lowerbound l \<bullet> k}) \<bullet> k = interval_lowerbound l \<bullet> k"
     unfolding l interval_split[OF k] interval_bounds[OF uv(1)]
@@ -1406,11 +1370,7 @@
   have "\<exists>x. x \<in> ?D - ?D1"
     using assms(3-)
     unfolding division_points_def interval_bounds[OF ab]
-    apply -
-    apply (erule disjE)
-    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
-    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
-    done           
+    by (force simp add: *)
   moreover have "?D1 \<subseteq> ?D"
     by (auto simp add: assms division_points_subset)
   ultimately show "?D1 \<subset> ?D"
@@ -1423,11 +1383,7 @@
   have "\<exists>x. x \<in> ?D - ?D2"
     using assms(3-)
     unfolding division_points_def interval_bounds[OF ab]
-    apply -
-    apply (erule disjE)
-    apply (rule_tac x="(k,(interval_lowerbound l)\<bullet>k)" in exI, force simp add: *)
-    apply (rule_tac x="(k,(interval_upperbound l)\<bullet>k)" in exI, force simp add: *)
-    done
+    by (force simp add: *)
   moreover have "?D2 \<subseteq> ?D"
     by (auto simp add: assms division_points_subset)
   ultimately show "?D2 \<subset> ?D"
@@ -1769,39 +1725,28 @@
     done
 next
   fix a b c :: real
-  assume "\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1"
-    and "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
+  assume eq1: "\<forall>a b. b \<le> a \<longrightarrow> g {a .. b} = \<^bold>1"
+    and eqg: "\<forall>a b c. a < c \<and> c < b \<longrightarrow> g {a..c} \<^bold>* g {c..b} = g {a..b}"
     and "a \<le> c"
     and "c \<le> b"
-  note as = this[rule_format]
   show "g {a..c} \<^bold>* g {c..b} = g {a..b}"
   proof (cases "c = a \<or> c = b")
     case False
     then show ?thesis
-      apply -
-      apply (subst as(2))
-      using as(3-)
-      apply auto
-      done
+      using eqg \<open>a \<le> c\<close> \<open>c \<le> b\<close> by auto
   next
     case True
     then show ?thesis
     proof
       assume *: "c = a"
       then have "g {a .. c} = \<^bold>1"
-        apply -
-        apply (rule as(1)[rule_format])
-        apply auto
-        done
+        using eq1 by blast
       then show ?thesis
         unfolding * by auto
     next
       assume *: "c = b"
       then have "g {c .. b} = \<^bold>1"
-        apply -
-        apply (rule as(1)[rule_format])
-        apply auto
-        done
+        using eq1 by blast
       then show ?thesis
         unfolding * by auto
     qed
@@ -1934,18 +1879,18 @@
 subsection \<open>Some basic combining lemmas.\<close>
 
 lemma tagged_division_Union_exists:
-  assumes "finite iset"
-    and "\<forall>i\<in>iset. \<exists>p. p tagged_division_of i \<and> d fine p"
-    and "\<forall>i1\<in>iset. \<forall>i2\<in>iset. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}"
-    and "\<Union>iset = i"
+  assumes "finite I"
+    and "\<forall>i\<in>I. \<exists>p. p tagged_division_of i \<and> d fine p"
+    and "\<forall>i1\<in>I. \<forall>i2\<in>I. i1 \<noteq> i2 \<longrightarrow> interior i1 \<inter> interior i2 = {}"
+    and "\<Union>I = i"
    obtains p where "p tagged_division_of i" and "d fine p"
 proof -
   obtain pfn where pfn:
-    "\<And>x. x \<in> iset \<Longrightarrow> pfn x tagged_division_of x"
-    "\<And>x. x \<in> iset \<Longrightarrow> d fine pfn x"
+    "\<And>x. x \<in> I \<Longrightarrow> pfn x tagged_division_of x"
+    "\<And>x. x \<in> I \<Longrightarrow> d fine pfn x"
     using bchoice[OF assms(2)] by auto
   show thesis
-    apply (rule_tac p="\<Union>(pfn ` iset)" in that)
+    apply (rule_tac p="\<Union>(pfn ` I)" in that)
     using assms(1) assms(3) assms(4) pfn(1) tagged_division_unions apply force
     by (metis (mono_tags, lifting) fine_Union imageE pfn(2))
 qed
@@ -1972,25 +1917,22 @@
     using assms(1,3) by metis
   then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
     by (force simp: mem_box)
-  { fix f
-    have "\<lbrakk>finite f;
+  have UN_cases: "\<lbrakk>finite f;
            \<And>s. s\<in>f \<Longrightarrow> P s;
            \<And>s. s\<in>f \<Longrightarrow> \<exists>a b. s = cbox a b;
-           \<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>f)"
-    proof (induct f rule: finite_induct)
-      case empty
-      show ?case
-        using assms(1) by auto
-    next
-      case (insert x f)
-      show ?case
-        unfolding Union_insert
-        apply (rule assms(2)[rule_format])
-        using Int_interior_Union_intervals [of f "interior x"]
-        apply (auto simp: insert)
-        by (metis IntI empty_iff insert.hyps(2) insert.prems(3) insert_iff)
-    qed
-  } note UN_cases = this
+           \<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>f)" for f
+  proof (induct f rule: finite_induct)
+    case empty
+    show ?case
+      using assms(1) by auto
+  next
+    case (insert x f)
+    show ?case
+      unfolding Union_insert
+      apply (rule assms(2)[rule_format])
+      using Int_interior_Union_intervals [of f "interior x"]
+      by (metis (no_types, lifting) insert insert_iff open_interior)
+  qed
   let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or>
     (c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}"
   let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
@@ -2110,13 +2052,12 @@
       then show "\<exists>c d. ?P i c d"
         by blast
     qed
+    then obtain \<alpha> \<beta> where
+     "\<forall>i\<in>Basis. (\<alpha> \<bullet> i = a \<bullet> i \<and> \<beta> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
+         \<alpha> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> \<beta> \<bullet> i = b \<bullet> i) \<and> \<alpha> \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> \<beta> \<bullet> i"
+      by (auto simp: choice_Basis_iff)
     then show "x\<in>\<Union>?A"
-      unfolding Union_iff Bex_def mem_Collect_eq choice_Basis_iff
-      apply auto
-      apply (rule_tac x="cbox xa xaa" in exI)
-      unfolding mem_box
-      apply auto
-      done
+      by (force simp add: mem_box)
   qed
   finally show False
     using assms by auto
@@ -2148,10 +2089,7 @@
            2 * (d \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i"
         by (rule interval_bisection_step[of P, OF assms(1-2) as])
       then show ?thesis
-        apply -
-        apply (rule_tac x="(c,d)" in exI)
-        apply auto
-        done
+        by (rule_tac x="(c,d)" in exI) auto
     qed
   qed
   then obtain f where f:
@@ -2162,11 +2100,7 @@
             fst x \<bullet> i \<le> fst (f x) \<bullet> i \<and>
             fst (f x) \<bullet> i \<le> snd (f x) \<bullet> i \<and>
             snd (f x) \<bullet> i \<le> snd x \<bullet> i \<and>
-            2 * (snd (f x) \<bullet> i - fst (f x) \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i)"
-    apply -
-    apply (drule choice)
-    apply blast
-    done
+            2 * (snd (f x) \<bullet> i - fst (f x) \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i)" by metis
   define AB A B where ab_def: "AB n = (f ^^ n) (a,b)" "A n = fst(AB n)" "B n = snd(AB n)" for n
   have [simp]: "A 0 = a" "B 0 = b" and ABRAW: "\<And>n. \<not> P (cbox (A(Suc n)) (B(Suc n))) \<and>
     (\<forall>i\<in>Basis. A(n)\<bullet>i \<le> A(Suc n)\<bullet>i \<and> A(Suc n)\<bullet>i \<le> B(Suc n)\<bullet>i \<and> B(Suc n)\<bullet>i \<le> B(n)\<bullet>i \<and>
@@ -2179,10 +2113,7 @@
     proof (induct n)
       case 0
       then show ?case
-        unfolding S
-        apply (rule f[rule_format]) using assms(3)
-        apply auto
-        done
+        unfolding S using \<open>\<not> P (cbox a b)\<close> f by auto
     next
       case (Suc n)
       show ?case
@@ -2230,8 +2161,7 @@
         next
           case (Suc n)
           have "B (Suc n) \<bullet> i - A (Suc n) \<bullet> i \<le> (B n \<bullet> i - A n \<bullet> i) / 2"
-            using AB(3) that
-            using AB(4)[of i n] using i by auto
+            using AB(3) that AB(4)[of i n] using i by auto
           also have "\<dots> \<le> (b \<bullet> i - a \<bullet> i) / 2 ^ Suc n"
             using Suc by (auto simp add: field_simps)
           finally show ?case .
@@ -2295,13 +2225,13 @@
   fixes a b :: "'a::euclidean_space"
   assumes "gauge g"
   obtains p where "p tagged_division_of (cbox a b)" "g fine p"
-proof -
-  presume "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p) \<Longrightarrow> False"
-  then obtain p where "p tagged_division_of (cbox a b)" "g fine p"
-    by blast
-  then show thesis ..
+proof (cases "\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p")
+  case True
+  then show ?thesis
+    using that by auto
 next
-  assume as: "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p)"
+  case False
+  assume "\<not> (\<exists>p. p tagged_division_of (cbox a b) \<and> g fine p)"
   obtain x where x:
       "x \<in> (cbox a b)"
       "\<And>e. 0 < e \<Longrightarrow>
@@ -2310,10 +2240,10 @@
           cbox c d \<subseteq> ball x e \<and>
           cbox c d \<subseteq> (cbox a b) \<and>
           \<not> (\<exists>p. p tagged_division_of cbox c d \<and> g fine p)"
-    apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ as])
+    apply (rule interval_bisection[of "\<lambda>s. \<exists>p. p tagged_division_of s \<and> g fine p", OF _ _ False])
     apply (simp add: fine_def)
     apply (metis tagged_division_union fine_Un)
-    apply (auto simp: )
+    apply auto
     done
   obtain e where e: "e > 0" "ball x e \<subseteq> g x"
     using gaugeD[OF assms, of x] unfolding open_contains_ball by auto
@@ -2325,7 +2255,7 @@
     by blast
   have "g fine {(x, cbox c d)}"
     unfolding fine_def using e using c_d(2) by auto
-  then show False
+  then show ?thesis
     using tagged_division_of_self[OF c_d(1)] using c_d by auto
 qed
 
@@ -2369,70 +2299,52 @@
   proof (induct p)
     case empty
     show ?case
-      apply (rule_tac x="{}" in exI)
-      unfolding fine_def
-      apply auto
-      done
+      by (force simp add: fine_def)
   next
     case (insert xk p)
-    guess x k using surj_pair[of xk] by (elim exE) note xk=this
-    note tagged_partial_division_subset[OF insert(4) subset_insertI]
-    from insert(3)[OF this insert(5)] 
+    obtain x k where xk: "xk = (x, k)"
+      using surj_pair[of xk] by metis 
     obtain q1 where q1: "q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}"
                 and "d fine q1"
                 and q1I: "\<And>x k. \<lbrakk>(x, k)\<in>p;  k \<subseteq> d x\<rbrakk> \<Longrightarrow> (x, k) \<in> q1"
-      by (force simp add: )
+      using case_prodD tagged_partial_division_subset[OF insert(4) subset_insertI]
+      by (metis (mono_tags, lifting) insert.hyps(3) insert.prems(2))
     have *: "\<Union>{l. \<exists>y. (y,l) \<in> insert xk p} = k \<union> \<Union>{l. \<exists>y. (y,l) \<in> p}"
       unfolding xk by auto
     note p = tagged_partial_division_ofD[OF insert(4)]
-    from p(4)[unfolded xk, OF insertI1] guess u v by (elim exE) note uv=this
-
+    obtain u v where uv: "k = cbox u v"
+      using p(4)[unfolded xk, OF insertI1] by blast
     have "finite {k. \<exists>x. (x, k) \<in> p}"
       apply (rule finite_subset[of _ "snd ` p"])
-      using p
-      apply safe
-      apply (metis image_iff snd_conv)
-      apply auto
-      done
+      using image_iff apply fastforce
+      using insert.hyps(1) by blast
     then have int: "interior (cbox u v) \<inter> interior (\<Union>{k. \<exists>x. (x, k) \<in> p}) = {}"
-      apply (rule Int_interior_Union_intervals)
-      apply (rule open_interior)
-      unfolding mem_Collect_eq
-      apply (erule_tac[!] exE)
-      apply (drule p(4)[OF insertI2])
-      apply assumption
-      apply (rule p(5))
-      unfolding uv xk
-      apply (rule insertI1)
-      apply (rule insertI2)
-      apply assumption
-      using insert(2)
-      unfolding uv xk
-      apply auto
-      done
+    proof (rule Int_interior_Union_intervals)
+      show "open (interior (cbox u v))"
+        by auto
+      show "\<And>T. T \<in> {k. \<exists>x. (x, k) \<in> p} \<Longrightarrow> \<exists>a b. T = cbox a b"
+        using p(4) by auto
+      show "\<And>T. T \<in> {k. \<exists>x. (x, k) \<in> p} \<Longrightarrow> interior (cbox u v) \<inter> interior T = {}"
+        by clarify (metis insert.hyps(2) insert_iff interior_cbox p(5) uv xk)
+    qed
     show ?case
     proof (cases "cbox u v \<subseteq> d x")
       case True
-      then show ?thesis
+      have "{(x, cbox u v)} tagged_division_of cbox u v"
+        by (simp add: p(2) uv xk tagged_division_of_self)
+      then have "{(x, cbox u v)} \<union> q1 tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> insert xk p}"
+        unfolding * uv by (metis (no_types, lifting) int q1 tagged_division_union)
+      with True show ?thesis
         apply (rule_tac x="{(x,cbox u v)} \<union> q1" in exI)
-        apply rule
-        unfolding * uv
-        apply (rule tagged_division_union)
-        apply (rule tagged_division_of_self)
-        apply (rule p[unfolded xk uv] insertI1)+
-        apply (rule q1)
-        apply (rule int)
-        apply rule
-        apply (rule fine_Un)
-        apply (subst fine_def)
-         apply (auto simp add:  \<open>d fine q1\<close> q1I uv xk)
+        using \<open>d fine q1\<close> fine_def q1I uv xk apply fastforce
         done
     next
       case False
-      from fine_division_exists[OF assms(2), of u v] guess q2 . note q2=this
+      obtain q2 where q2: "q2 tagged_division_of cbox u v" "d fine q2"
+        using fine_division_exists[OF assms(2)] by blast
       show ?thesis
         apply (rule_tac x="q2 \<union> q1" in exI)
-        apply rule
+        apply (intro conjI)
         unfolding * uv
         apply (rule tagged_division_union q2 q1 int fine_Un)+
           apply (auto intro: q1 q2 fine_Un \<open>d fine q1\<close> simp add: False q1I uv xk)
--- a/src/HOL/Library/Multiset.thy	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Aug 04 18:03:50 2017 +0200
@@ -3458,8 +3458,7 @@
 
 end
 
-lemma [code]: "sum_mset (mset xs) = sum_list xs"
-  by (induct xs) simp_all
+declare sum_mset_sum_list [code]
 
 lemma [code]: "prod_mset (mset xs) = fold times xs 1"
 proof -
--- a/src/HOL/SMT.thy	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/HOL/SMT.thy	Fri Aug 04 18:03:50 2017 +0200
@@ -246,7 +246,7 @@
 \<close>
 
 declare [[cvc3_options = ""]]
-declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant"]]
+declare [[cvc4_options = "--full-saturate-quant --inst-when=full-last-call --inst-no-entail --term-db-mode=relevant --multi-trigger-linear"]]
 declare [[verit_options = ""]]
 declare [[z3_options = ""]]
 
--- a/src/HOL/Statespace/state_space.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/HOL/Statespace/state_space.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -298,7 +298,7 @@
 
 fun add_declaration name decl thy =
   thy
-  |> Named_Target.init NONE name
+  |> Named_Target.init name
   |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy)
   |> Local_Theory.exit_global;
 
--- a/src/HOL/String.thy	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/HOL/String.thy	Fri Aug 04 18:03:50 2017 +0200
@@ -16,6 +16,8 @@
   show "Suc 0 \<in> {n. n < 256}" by simp
 qed
 
+setup_lifting type_definition_char
+
 definition char_of_nat :: "nat \<Rightarrow> char"
 where
   "char_of_nat n = Abs_char (n mod 256)"
@@ -304,6 +306,9 @@
   "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
   by (simp add: char_of_integer_def enum_char_unfold)
 
+lifting_update char.lifting
+lifting_forget char.lifting
+
 
 subsection \<open>Strings as dedicated type\<close>
 
--- a/src/HOL/Tools/code_evaluation.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -20,8 +20,9 @@
 
 (* formal definition *)
 
-fun add_term_of tyco raw_vs thy =
+fun add_term_of_inst tyco thy =
   let
+    val ((raw_vs, _), _) = Code.get_type thy tyco;
     val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
     val ty = Type (tyco, map TFree vs);
     val lhs = Const (@{const_name term_of}, ty --> @{typ term})
@@ -39,11 +40,11 @@
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end;
 
-fun ensure_term_of (tyco, (vs, _)) thy =
+fun ensure_term_of_inst tyco thy =
   let
     val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of})
       andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep};
-  in if need_inst then add_term_of tyco vs thy else thy end;
+  in if need_inst then add_term_of_inst tyco thy else thy end;
 
 fun for_term_of_instance tyco vs f thy =
   let
@@ -74,20 +75,19 @@
     |> Thm.varifyT_global
   end;
 
-fun add_term_of_code tyco vs raw_cs thy =
+fun add_term_of_code_datatype tyco vs raw_cs thy =
   let
     val ty = Type (tyco, map TFree vs);
     val cs = (map o apsnd o apsnd o map o map_atyps)
       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
-    val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
     val eqs = map (mk_term_of_eq thy ty) cs;
  in
     thy
     |> Code.declare_default_eqns_global (map (rpair true) eqs)
   end;
 
-fun ensure_term_of_code (tyco, (vs, cs)) =
-  for_term_of_instance tyco vs (fn tyco => fn vs => add_term_of_code tyco vs cs);
+fun ensure_term_of_code_datatype (tyco, (vs, cs)) =
+  for_term_of_instance tyco vs (fn tyco => fn vs => add_term_of_code_datatype tyco vs cs);
 
 
 (* code equations for abstypes *)
@@ -105,31 +105,29 @@
     |> Thm.varifyT_global
   end;
 
-fun add_abs_term_of_code tyco vs abs raw_ty_rep proj thy =
+fun add_term_of_code_abstype tyco vs abs raw_ty_rep projection thy =
   let
     val ty = Type (tyco, map TFree vs);
     val ty_rep = map_atyps
       (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
-    val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
-    val eq = mk_abs_term_of_eq thy ty abs ty_rep proj;
+    val eq = mk_abs_term_of_eq thy ty abs ty_rep projection;
  in
     thy
     |> Code.declare_default_eqns_global [(eq, true)]
   end;
 
-fun ensure_abs_term_of_code (tyco, (vs, {abstractor = (abs, (_, ty)),
+fun ensure_term_of_code_abstype (tyco, (vs, {abstractor = (abs, (_, ty)),
     projection, ...})) =
   for_term_of_instance tyco vs
-    (fn tyco => fn vs => add_abs_term_of_code tyco vs abs ty projection);
+    (fn tyco => fn vs => add_term_of_code_abstype tyco vs abs ty projection);
 
 
 (* setup *)
 
 val _ = Theory.setup
-  (Code.datatype_interpretation ensure_term_of
-  #> Code.abstype_interpretation ensure_term_of
-  #> Code.datatype_interpretation ensure_term_of_code
-  #> Code.abstype_interpretation ensure_abs_term_of_code);
+  (Code.type_interpretation ensure_term_of_inst
+  #> Code.datatype_interpretation ensure_term_of_code_datatype
+  #> Code.abstype_interpretation ensure_term_of_code_abstype);
 
 
 (** termifying syntax **)
--- a/src/HOL/Typerep.thy	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/HOL/Typerep.thy	Fri Aug 04 18:03:50 2017 +0200
@@ -72,8 +72,7 @@
 
 add_typerep @{type_name fun}
 #> Typedef.interpretation (Local_Theory.background_theory o ensure_typerep)
-#> Code.datatype_interpretation (ensure_typerep o fst)
-#> Code.abstype_interpretation (ensure_typerep o fst)
+#> Code.type_interpretation ensure_typerep
 
 end
 \<close>
--- a/src/Pure/Isar/bundle.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Pure/Isar/bundle.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -175,18 +175,17 @@
 
 fun init binding thy =
   thy
-  |> Sign.change_begin
-  |> set_target []
-  |> Proof_Context.init_global
-  |> Local_Theory.init (Sign.naming_of thy)
+  |> Generic_Target.init
+     {background_naming = Sign.naming_of thy,
+      setup = set_target [] #> Proof_Context.init_global,
+      conclude = conclude false binding #> #2}
      {define = bad_operation,
       notes = bundle_notes,
       abbrev = bad_operation,
       declaration = K bundle_declaration,
       theory_registration = bad_operation,
       locale_dependency = bad_operation,
-      pretty = pretty binding,
-      exit = conclude false binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local}
+      pretty = pretty binding}
 
 end;
 
@@ -216,7 +215,8 @@
       |> prep_decl ([], []) I raw_elems;
   in
     lthy' |> Local_Theory.init_target
-      (Local_Theory.background_naming_of lthy) (Local_Theory.operations_of lthy) after_close
+      {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close}
+      (Local_Theory.operations_of lthy)
   end;
 
 in
--- a/src/Pure/Isar/class.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Pure/Isar/class.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -683,26 +683,26 @@
       | NONE => NONE);
   in
     thy
-    |> Sign.change_begin
-    |> Proof_Context.init_global
-    |> Instantiation.put (make_instantiation ((tycos, vs, sort), params))
-    |> fold (Variable.declare_typ o TFree) vs
-    |> fold (Variable.declare_names o Free o snd) params
-    |> (Overloading.map_improvable_syntax) (K {primary_constraints = primary_constraints,
-      secondary_constraints = [], improve = improve, subst = K NONE,
-      no_subst_in_abbrev_mode = false, unchecks = []})
-    |> Overloading.activate_improvable_syntax
-    |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
-    |> synchronize_inst_syntax
-    |> Local_Theory.init (Sign.naming_of thy)
+    |> Generic_Target.init
+       {background_naming = Sign.naming_of thy,
+        setup = Proof_Context.init_global
+          #> Instantiation.put (make_instantiation ((tycos, vs, sort), params))
+          #> fold (Variable.declare_typ o TFree) vs
+          #> fold (Variable.declare_names o Free o snd) params
+          #> (Overloading.map_improvable_syntax) (K {primary_constraints = primary_constraints,
+            secondary_constraints = [], improve = improve, subst = K NONE,
+            no_subst_in_abbrev_mode = false, unchecks = []})
+          #> Overloading.activate_improvable_syntax
+          #> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
+          #> synchronize_inst_syntax,
+        conclude = conclude}
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes Generic_Target.theory_target_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
         theory_registration = Generic_Target.theory_registration,
         locale_dependency = fn _ => error "Not possible in instantiation target",
-        pretty = pretty,
-        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+        pretty = pretty}
   end;
 
 fun instantiation_cmd arities thy =
--- a/src/Pure/Isar/class_declaration.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -327,7 +327,7 @@
     #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
     #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
     |> snd
-    |> Named_Target.init NONE class
+    |> Named_Target.init class
     |> pair class
   end;
 
--- a/src/Pure/Isar/code.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Pure/Isar/code.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -30,16 +30,15 @@
   val pretty_cert: theory -> cert -> Pretty.T list
 
   (*executable code*)
+  type constructors
+  type abs_type
+  val type_interpretation: (string -> theory -> theory) -> theory -> theory
+  val datatype_interpretation: (string * constructors -> theory -> theory) -> theory -> theory
+  val abstype_interpretation: (string * abs_type -> theory -> theory) -> theory -> theory
   val declare_datatype_global: (string * typ) list -> theory -> theory
   val declare_datatype_cmd: string list -> theory -> theory
-  val datatype_interpretation:
-    (string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
-      -> theory -> theory) -> theory -> theory
   val declare_abstype: thm -> local_theory -> local_theory
   val declare_abstype_global: thm -> theory -> theory
-  val abstype_interpretation:
-    (string * ((string * sort) list * {abs_rep: thm, abstractor: string * ((string * sort) list * typ),
-      projection: string}) -> theory -> theory) -> theory -> theory
   val declare_default_eqns: (thm * bool) list -> local_theory -> local_theory
   val declare_default_eqns_global: (thm * bool) list -> theory -> theory
   val declare_eqns: (thm * bool) list -> local_theory -> local_theory
@@ -52,8 +51,7 @@
   val declare_unimplemented_global: string -> theory -> theory
   val declare_case_global: thm -> theory -> theory
   val declare_undefined_global: string -> theory -> theory
-  val get_type: theory -> string
-    -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool
+  val get_type: theory -> string -> constructors * bool
   val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
   val is_constr: theory -> string -> bool
   val is_abstr: theory -> string -> bool
@@ -277,9 +275,6 @@
 
 local
 
-fun tap_serial (table : 'a T) key =
-  Option.map (hd o #history) (Symtab.lookup table key);
-
 fun merge_history join_same
     ({entry = entry1, history = history1, ...}, {entry = entry2, history = history2, ...}) =
   let
@@ -338,7 +333,7 @@
           NONE => false
         | SOME (_, Abstractor {abstractor = (abs', _), projection, more_abstract_functions, ...}) =>
             abs = abs' andalso (c = projection orelse member (op =) more_abstract_functions c));
-    fun check_datatypes (c, case_spec) =
+    fun check_datatypes (_, case_spec) =
       let
         val (tycos, required_constructors) = associated_datatypes case_spec;
         val allowed_constructors =
@@ -348,10 +343,6 @@
       in subset (op =) (required_constructors, allowed_constructors) end;
     val all_constructors =
       maps (fst o constructors_of) all_types;
-    val all_abstract_functions =
-      maps abstract_functions_of all_types;
-    val case_combinators =
-      maps case_combinators_of all_types;
     val functions = History.join fst (functions1, functions2)
       |> fold (History.suppress o fst) all_constructors
       |> History.suppress_except check_abstype;
@@ -552,6 +543,9 @@
 
 fun lookup_vs_type_spec thy = History.lookup ((types_of o specs_of) thy);
 
+type constructors =
+  (string * sort) list * (string * ((string * sort) list * typ list)) list;
+
 fun get_type thy tyco = case lookup_vs_type_spec thy tyco
  of SOME (vs, type_spec) => apfst (pair vs) (constructors_of type_spec)
   | NONE => Sign.arity_number thy tyco
@@ -560,6 +554,9 @@
       |> rpair []
       |> rpair false;
 
+type abs_type =
+  (string * sort) list * {abs_rep: thm, abstractor: string * ((string * sort) list * typ), projection: string};
+
 fun get_abstype_spec thy tyco = case lookup_vs_type_spec thy tyco of
     SOME (vs, Abstractor {abs_rep, abstractor, projection, ...}) =>
       (vs, {abs_rep = abs_rep, abstractor = abstractor, projection = projection})
@@ -1003,7 +1000,7 @@
       Nothing (constrain_cert_thm thy sorts cert_thm)
   | constrain_cert thy sorts (Equations (cert_thm, propers)) =
       Equations (constrain_cert_thm thy sorts cert_thm, propers)
-  | constrain_cert thy _ (cert as Projection _) =
+  | constrain_cert _ _ (cert as Projection _) =
       cert
   | constrain_cert thy sorts (Abstract (abs_thm, tyco)) =
       Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco);
@@ -1074,8 +1071,8 @@
           (SOME (Thm.varifyT_global abs_thm), true))])
       end;
 
-fun pretty_cert thy (cert as Nothing _) =
-      [Pretty.str "(unimplemented)"]
+fun pretty_cert _ (Nothing _) =
+      []
   | pretty_cert thy (cert as Equations _) =
       (map_filter
         (Option.map (Thm.pretty_thm_global thy o
@@ -1263,6 +1260,40 @@
 
 (** declaration of executable ingredients **)
 
+(* plugins for dependent applications *)
+
+structure Codetype_Plugin = Plugin(type T = string);
+
+val codetype_plugin = Plugin_Name.declare_setup @{binding codetype};
+
+fun type_interpretation f =
+  Codetype_Plugin.interpretation codetype_plugin
+    (fn tyco => Local_Theory.background_theory
+      (fn thy =>
+        thy
+        |> Sign.root_path
+        |> Sign.add_path (Long_Name.qualifier tyco)
+        |> f tyco 
+        |> Sign.restore_naming thy));
+
+fun datatype_interpretation f =
+  type_interpretation (fn tyco => fn thy =>
+    case get_type thy tyco of
+      (spec, false) => f (tyco, spec) thy
+    | (_, true) => thy
+  );
+
+fun abstype_interpretation f =
+  type_interpretation (fn tyco => fn thy =>
+    case try (get_abstype_spec thy) tyco of
+      SOME spec => f (tyco, spec) thy
+    | NONE => thy
+  );
+
+fun register_tyco_for_plugin tyco =
+  Named_Target.theory_map (Codetype_Plugin.data_default tyco);
+
+
 (* abstract code declarations *)
 
 local
@@ -1302,19 +1333,6 @@
     |> map_types (History.register tyco vs_typ_spec)
   end;
 
-structure Datatype_Plugin = Plugin(type T = string);
-
-val datatype_plugin = Plugin_Name.declare_setup @{binding datatype_code};
-
-fun datatype_interpretation f =
-  Datatype_Plugin.interpretation datatype_plugin
-    (fn tyco => Local_Theory.background_theory (fn thy =>
-      thy
-      |> Sign.root_path
-      |> Sign.add_path (Long_Name.qualifier tyco)
-      |> f (tyco, fst (get_type thy tyco))
-      |> Sign.restore_naming thy));
-
 fun declare_datatype_global proto_constrs thy =
   let
     fun unoverload_const_typ (c, ty) =
@@ -1325,21 +1343,12 @@
     thy
     |> modify_specs (register_type
         (tyco, (vs, Constructors {constructors = cos, case_combinators = []})))
-    |> Named_Target.theory_map (Datatype_Plugin.data_default tyco)
+    |> register_tyco_for_plugin tyco
   end;
 
 fun declare_datatype_cmd raw_constrs thy =
   declare_datatype_global (map (read_bare_const thy) raw_constrs) thy;
 
-structure Abstype_Plugin = Plugin(type T = string);
-
-val abstype_plugin = Plugin_Name.declare_setup @{binding abstype_code};
-
-fun abstype_interpretation f =
-  Abstype_Plugin.interpretation abstype_plugin
-    (fn tyco =>
-      Local_Theory.background_theory (fn thy => f (tyco, get_abstype_spec thy tyco) thy));
-
 fun generic_declare_abstype strictness proto_thm thy =
   case check_abstype_cert strictness thy proto_thm of
     SOME (tyco, (vs, (abstractor as (abs, (_, ty)), (proj, abs_rep)))) =>
@@ -1348,7 +1357,7 @@
             (tyco, (vs, Abstractor {abstractor = abstractor, projection = proj, abs_rep = abs_rep, more_abstract_functions = []}))
           #> register_fun_spec proj
             (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs proj), (tyco, abs))))
-      |> Named_Target.theory_map (Abstype_Plugin.data_default tyco)
+      |> register_tyco_for_plugin tyco
   | NONE => thy;
 
 val declare_abstype_global = generic_declare_abstype Strict;
--- a/src/Pure/Isar/expression.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Pure/Isar/expression.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -825,7 +825,7 @@
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps')
-      |> Named_Target.init NONE name
+      |> Named_Target.init name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
--- a/src/Pure/Isar/generic_target.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Pure/Isar/generic_target.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -76,6 +76,11 @@
     local_theory -> local_theory
   val locale_dependency: string -> string * morphism -> (morphism * bool) option -> morphism ->
     local_theory -> local_theory
+
+  (*initialisation*)
+  val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
+    conclude: local_theory -> local_theory} ->
+    Local_Theory.operations -> theory -> local_theory
 end
 
 structure Generic_Target: GENERIC_TARGET =
@@ -417,4 +422,16 @@
 
 fun locale_abbrev locale = abbrev (locale_target_abbrev locale);
 
+
+(** initialisation **)
+
+fun init {background_naming, setup, conclude} operations thy =
+  thy
+  |> Sign.change_begin
+  |> setup
+  |> Local_Theory.init
+      {background_naming = background_naming,
+       exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+      operations;
+
 end;
--- a/src/Pure/Isar/interpretation.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Pure/Isar/interpretation.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -220,7 +220,7 @@
 fun gen_global_sublocale prep_loc prep_interpretation
     raw_locale expression raw_defs raw_eqns thy =
   let
-    val lthy = Named_Target.init NONE (prep_loc thy raw_locale) thy;
+    val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
     fun setup_proof after_qed =
       Element.witness_proof_eqs
         (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
--- a/src/Pure/Isar/local_theory.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Pure/Isar/local_theory.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -65,13 +65,14 @@
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
-  val init: Name_Space.naming -> operations -> Proof.context -> local_theory
+  val init: {background_naming: Name_Space.naming, exit: local_theory -> Proof.context} ->
+    operations -> Proof.context -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
-  val init_target: Name_Space.naming -> operations -> (local_theory -> local_theory) ->
-    local_theory -> Binding.scope * local_theory
+  val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory} ->
+    operations -> local_theory -> Binding.scope * local_theory
   val open_target: local_theory -> Binding.scope * local_theory
   val close_target: local_theory -> local_theory
 end;
@@ -95,19 +96,19 @@
      local_theory -> local_theory,
   locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
      local_theory -> local_theory,
-  pretty: local_theory -> Pretty.T list,
-  exit: local_theory -> Proof.context};
+  pretty: local_theory -> Pretty.T list};
 
 type lthy =
  {background_naming: Name_Space.naming,
   operations: operations,
   after_close: local_theory -> local_theory,
+  exit: local_theory -> Proof.context,
   brittle: bool,
   target: Proof.context};
 
-fun make_lthy (background_naming, operations, after_close, brittle, target) : lthy =
+fun make_lthy (background_naming, operations, after_close, exit, brittle, target) : lthy =
   {background_naming = background_naming, operations = operations,
-    after_close = after_close, brittle = brittle, target = target};
+    after_close = after_close, exit = exit, brittle = brittle, target = target};
 
 
 (* context data *)
@@ -146,16 +147,16 @@
 
 fun map_top f =
   assert #>
-  Data.map (fn {background_naming, operations, after_close, brittle, target} :: parents =>
-    make_lthy (f (background_naming, operations, after_close, brittle, target)) :: parents);
+  Data.map (fn {background_naming, operations, after_close, exit, brittle, target} :: parents =>
+    make_lthy (f (background_naming, operations, after_close, exit, brittle, target)) :: parents);
 
 fun reset lthy = #target (top_of lthy) |> Data.put (Data.get lthy);
 
 fun map_contexts f lthy =
   let val n = level lthy in
     lthy |> (Data.map o map_index)
-      (fn (i, {background_naming, operations, after_close, brittle, target}) =>
-        make_lthy (background_naming, operations, after_close, brittle,
+      (fn (i, {background_naming, operations, after_close, exit, brittle, target}) =>
+        make_lthy (background_naming, operations, after_close, exit, brittle,
           target
           |> Context_Position.set_visible false
           |> f (n - i - 1)
@@ -168,8 +169,8 @@
 
 fun mark_brittle lthy =
   if level lthy = 1 then
-    map_top (fn (background_naming, operations, after_close, _, target) =>
-      (background_naming, operations, after_close, true, target)) lthy
+    map_top (fn (background_naming, operations, after_close, exit, _, target) =>
+      (background_naming, operations, after_close, exit, true, target)) lthy
   else lthy;
 
 fun assert_nonbrittle lthy =
@@ -182,8 +183,8 @@
 val background_naming_of = #background_naming o top_of;
 
 fun map_background_naming f =
-  map_top (fn (background_naming, operations, after_close, brittle, target) =>
-    (f background_naming, operations, after_close, brittle, target));
+  map_top (fn (background_naming, operations, after_close, exit, brittle, target) =>
+    (f background_naming, operations, after_close, exit, brittle, target));
 
 val restore_background_naming = map_background_naming o K o background_naming_of;
 
@@ -348,12 +349,14 @@
 
 (* outermost target *)
 
-fun init background_naming operations target =
+fun init {background_naming, exit} operations target =
   target |> Data.map
-    (fn [] => [make_lthy (background_naming, operations, I, false, target)]
+    (fn [] => [make_lthy (background_naming, operations, I, exit, false, target)]
       | _ => error "Local theory already initialized");
 
-val exit = operation #exit;
+val exit_of = #exit o bottom_of;
+
+fun exit lthy = exit_of lthy lthy;
 val exit_global = Proof_Context.theory_of o exit;
 
 fun exit_result f (x, lthy) =
@@ -372,18 +375,19 @@
 
 (* nested targets *)
 
-fun init_target background_naming operations after_close lthy =
+fun init_target {background_naming, after_close} operations lthy =
   let
     val _ = assert lthy;
     val after_close' = Proof_Context.restore_naming lthy #> after_close;
     val (scope, target) = Proof_Context.new_scope lthy;
     val lthy' =
       target
-      |> Data.map (cons (make_lthy (background_naming, operations, after_close', true, target)));
+      |> Data.map (cons (make_lthy (background_naming, operations, after_close', exit_of lthy, true, target)));
   in (scope, lthy') end;
 
 fun open_target lthy =
-  init_target (background_naming_of lthy) (operations_of lthy) I lthy;
+  init_target {background_naming = background_naming_of lthy, after_close = I}
+    (operations_of lthy) lthy;
 
 fun close_target lthy =
   let
--- a/src/Pure/Isar/locale.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Pure/Isar/locale.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -88,6 +88,7 @@
   val print_locale: theory -> bool -> xstring * Position.T -> unit
   val print_registrations: Proof.context -> xstring * Position.T -> unit
   val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
+  val pretty_locale: theory -> bool -> string -> Pretty.T list
   val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list
 end;
 
@@ -699,13 +700,12 @@
       activate_all name thy cons_elem (K (Morphism.transfer_morphism thy)) (empty_idents, [])
       |> snd |> rev;
   in
-    Pretty.block
-      (Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
-        maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems)
+    Pretty.keyword1 "locale" :: Pretty.brk 1 :: pretty_name locale_ctxt name ::
+      maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt locale_ctxt elem)]) elems
   end;
 
 fun print_locale thy show_facts raw_name =
-  Pretty.writeln (pretty_locale thy show_facts (check thy raw_name));
+  Pretty.writeln (Pretty.block (pretty_locale thy show_facts (check thy raw_name)));
 
 fun print_registrations ctxt raw_name =
   let
@@ -732,7 +732,7 @@
     fun make_node name =
      {name = name,
       parents = map (fst o fst) (dependencies_of thy name),
-      body = pretty_locale thy false name};
+      body = Pretty.block (pretty_locale thy false name)};
     val names = sort_strings (Name_Space.fold_table (cons o #1) (Locales.get thy) []);
   in map make_node names end;
 
--- a/src/Pure/Isar/named_target.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Pure/Isar/named_target.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -2,7 +2,7 @@
     Author:     Makarius
     Author:     Florian Haftmann, TU Muenchen
 
-Targets for theory, locale, class -- at the bottom the nested structure.
+Targets for theory, locale, class -- at the bottom of the nested structure.
 *)
 
 signature NAMED_TARGET =
@@ -11,7 +11,9 @@
   val locale_of: local_theory -> string option
   val bottom_locale_of: local_theory -> string option
   val class_of: local_theory -> string option
-  val init: (local_theory -> local_theory) option -> string -> theory -> local_theory
+  val init: string -> theory -> local_theory
+  val init': {setup: local_theory -> local_theory, conclude: local_theory -> local_theory} ->
+    string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val theory_map: (local_theory -> local_theory) -> theory -> theory
   val begin: xstring * Position.T -> theory -> local_theory
@@ -25,41 +27,53 @@
 
 (* context data *)
 
+datatype target = Theory | Locale of string | Class of string;
+
+fun target_of_ident _ "" = Theory
+  | target_of_ident thy ident =
+      if Locale.defined thy ident
+      then (if Class.is_class thy ident then Class else Locale) ident
+      else error ("No such locale: " ^ quote ident);
+
+fun ident_of_target Theory = ""
+  | ident_of_target (Locale locale) = locale
+  | ident_of_target (Class class) = class;
+
+fun target_is_theory (SOME Theory) = true
+  | target_is_theory _ = false;
+
+fun locale_of_target (SOME (Locale locale)) = SOME locale
+  | locale_of_target (SOME (Class locale)) = SOME locale
+  | locale_of_target _ = NONE;
+
+fun class_of_target (SOME (Class class)) = SOME class
+  | class_of_target _ = NONE;
+
 structure Data = Proof_Data
 (
-  type T = (string * bool) option;
+  type T = target option;
   fun init _ = NONE;
 );
 
-val get_bottom_data = Data.get;
+val get_bottom_target = Data.get;
 
-fun get_data lthy =
+fun get_target lthy =
   if Local_Theory.level lthy = 1
-  then get_bottom_data lthy
+  then get_bottom_target lthy
   else NONE;
 
-fun is_theory lthy =
-  (case get_data lthy of
-    SOME ("", _) => true
-  | _ => false);
-
-fun target_of lthy =
-  (case get_data lthy of
+fun ident_of lthy =
+  case get_target lthy of
     NONE => error "Not in a named target"
-  | SOME (target, _) => target);
+  | SOME target => ident_of_target target;
 
-fun locale_name_of NONE = NONE
-  | locale_name_of (SOME ("", _)) = NONE
-  | locale_name_of (SOME (locale, _)) = SOME locale;
+val is_theory = target_is_theory o get_target;
 
-val locale_of = locale_name_of o get_data;
+val locale_of = locale_of_target o get_target;
 
-val bottom_locale_of = locale_name_of o get_bottom_data;
+val bottom_locale_of = locale_of_target o get_bottom_target;
 
-fun class_of lthy =
-  (case get_data lthy of
-    SOME (class, true) => SOME class
-  | _ => NONE);
+val class_of = class_of_target o get_target;
 
 
 (* operations *)
@@ -74,94 +88,60 @@
   #-> (fn (lhs, def) => Class.const class ((b, mx), lhs) params
     #> pair (lhs, def));
 
-fun foundation ("", _) = Generic_Target.theory_target_foundation
-  | foundation (locale, false) = locale_foundation locale
-  | foundation (class, true) = class_foundation class;
-
-fun notes ("", _) = Generic_Target.theory_target_notes
-  | notes (locale, _) = Generic_Target.locale_target_notes locale;
-
-fun abbrev ("", _) = Generic_Target.theory_abbrev
-  | abbrev (locale, false) = Generic_Target.locale_abbrev locale
-  | abbrev (class, true) = Class.abbrev class;
-
-fun declaration ("", _) _ decl = Generic_Target.theory_declaration decl
-  | declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl;
-
-fun theory_registration ("", _) = Generic_Target.theory_registration
-  | theory_registration _ = (fn _ => error "Not possible in theory target");
-
-fun locale_dependency ("", false) = (fn _ => error "Not possible in locale target")
-  | locale_dependency ("", true) = (fn _ => error "Not possible in class target")
-  | locale_dependency (locale, _) = Generic_Target.locale_dependency locale;
+fun operations Theory =
+      {define = Generic_Target.define Generic_Target.theory_target_foundation,
+       notes = Generic_Target.notes Generic_Target.theory_target_notes,
+       abbrev = Generic_Target.theory_abbrev,
+       declaration = fn _ => Generic_Target.theory_declaration,
+       theory_registration = Generic_Target.theory_registration,
+       locale_dependency = fn _ => error "Not possible in theory target",
+       pretty = fn ctxt => [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
+        Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]}
+  | operations (Locale locale) =
+      {define = Generic_Target.define (locale_foundation locale),
+       notes = Generic_Target.notes (Generic_Target.locale_target_notes locale),
+       abbrev = Generic_Target.locale_abbrev locale,
+       declaration = Generic_Target.locale_declaration locale,
+       theory_registration = fn _ => error "Not possible in locale target",
+       locale_dependency = Generic_Target.locale_dependency locale,
+       pretty = fn ctxt => Locale.pretty_locale (Proof_Context.theory_of ctxt) false locale}
+  | operations (Class class) =
+      {define = Generic_Target.define (class_foundation class),
+       notes = Generic_Target.notes (Generic_Target.locale_target_notes class),
+       abbrev = Class.abbrev class,
+       declaration = Generic_Target.locale_declaration class,
+       theory_registration = fn _ => error "Not possible in class target",
+       locale_dependency = Generic_Target.locale_dependency class,
+       pretty = fn ctxt => Class.pretty_specification (Proof_Context.theory_of ctxt) class};
 
-fun pretty (target, is_class) ctxt =
-  if target = "" then
-    [Pretty.block [Pretty.keyword1 "theory", Pretty.brk 1,
-      Pretty.str (Context.theory_name (Proof_Context.theory_of ctxt))]]
-  else if is_class then Class.pretty_specification (Proof_Context.theory_of ctxt) target
-  else
-    (* FIXME pretty locale content *)
-    let
-      val target_name = [Pretty.keyword1 "locale", Pretty.brk 1, Locale.pretty_name ctxt target];
-      val fixes =
-        map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
-          (#1 (Proof_Context.inferred_fixes ctxt));
-      val assumes =
-        map (fn A => (Binding.empty_atts, [(Thm.term_of A, [])]))
-          (Assumption.all_assms_of ctxt);
-      val elems =
-        (if null fixes then [] else [Element.Fixes fixes]) @
-        (if null assumes then [] else [Element.Assumes assumes]);
-    in
-      if null elems then [Pretty.block target_name]
-      else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
-        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
-    end;
+fun setup_context Theory = Proof_Context.init_global
+  | setup_context (Locale locale) = Locale.init locale
+  | setup_context (Class class) = Class.init class;
 
-
-(* init *)
-
-fun make_name_data _ "" = ("", false)
-  | make_name_data thy target =
-      if Locale.defined thy target
-      then (target, Class.is_class thy target)
-      else error ("No such locale: " ^ quote target);
-
-fun init_context ("", _) = Proof_Context.init_global
-  | init_context (locale, false) = Locale.init locale
-  | init_context (class, true) = Class.init class;
-
-fun init before_exit target thy =
+fun init' {setup, conclude} ident thy =
   let
-    val name_data = make_name_data thy target;
-    val background_naming =
-      Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name target);
+    val target = target_of_ident thy ident;
   in
     thy
-    |> Sign.change_begin
-    |> init_context name_data
-    |> is_none before_exit ? Data.put (SOME name_data)
-    |> Local_Theory.init background_naming
-       {define = Generic_Target.define (foundation name_data),
-        notes = Generic_Target.notes (notes name_data),
-        abbrev = abbrev name_data,
-        declaration = declaration name_data,
-        theory_registration = theory_registration name_data,
-        locale_dependency = locale_dependency name_data,
-        pretty = pretty name_data,
-        exit = the_default I before_exit
-          #> Local_Theory.target_of #> Sign.change_end_local}
+    |> Generic_Target.init
+       {background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident),
+        setup = setup_context target #> setup,
+        conclude = conclude}
+       (operations target)
   end;
 
-val theory_init = init NONE "";
+fun init ident thy =
+  init' {setup = Data.put (SOME (target_of_ident thy ident)), conclude = I} ident thy;
+
+val theory_init = init "";
+
 fun theory_map f = theory_init #> f #> Local_Theory.exit_global;
 
 
 (* toplevel interaction *)
 
 fun begin ("-", _) thy = theory_init thy
-  | begin target thy = init NONE (Locale.check thy target) thy;
+  | begin target thy = init (Locale.check thy target) thy;
 
 val exit = Local_Theory.assert_bottom #> Local_Theory.exit_global;
 
@@ -172,7 +152,7 @@
   | switch NONE (Context.Proof lthy) =
       (Context.Proof o Local_Theory.reset, lthy)
   | switch (SOME name) (Context.Proof lthy) =
-      (Context.Proof o init NONE (target_of lthy) o exit,
+      (Context.Proof o init (ident_of lthy) o exit,
         (begin name o exit o Local_Theory.assert_nonbrittle) lthy);
 
 end;
--- a/src/Pure/Isar/overloading.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Pure/Isar/overloading.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -193,21 +193,21 @@
       (Term.dest_Const (prep_const ctxt const), (v, checked)));
   in
     thy
-    |> Sign.change_begin
-    |> Proof_Context.init_global
-    |> Data.put overloading
-    |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
-    |> activate_improvable_syntax
-    |> synchronize_syntax
-    |> Local_Theory.init (Sign.naming_of thy)
+    |> Generic_Target.init
+       {background_naming = Sign.naming_of thy,
+        setup = Proof_Context.init_global
+          #> Data.put overloading
+          #> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
+          #> activate_improvable_syntax
+          #> synchronize_syntax,
+        conclude = conclude}
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes Generic_Target.theory_target_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
         theory_registration = Generic_Target.theory_registration,
         locale_dependency = fn _ => error "Not possible in overloading target",
-        pretty = pretty,
-        exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
+        pretty = pretty}
   end;
 
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
--- a/src/Tools/Code/code_ml.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Tools/Code/code_ml.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -59,7 +59,6 @@
 fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   let
     val deresolve_const = deresolve o Constant;
-    val deresolve_class = deresolve o Type_Class;
     val deresolve_classrel = deresolve o Class_Relation;
     val deresolve_inst = deresolve o Class_Instance;
     fun print_tyco_expr (sym, []) = (str o deresolve) sym
@@ -372,7 +371,6 @@
 fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
   let
     val deresolve_const = deresolve o Constant;
-    val deresolve_class = deresolve o Type_Class;
     val deresolve_classrel = deresolve o Class_Relation;
     val deresolve_inst = deresolve o Class_Instance;
     fun print_tyco_expr (sym, []) = (str o deresolve) sym
@@ -676,6 +674,8 @@
           in pair
            (if Code_Namespace.is_public export
               then type_decl_p :: map print_classparam_decl classparams
+              else if null classrels andalso null classparams
+              then [type_decl_p] (*work around weakness in export calculation*)
               else [concat [str "type", print_dicttyp (class, ITyVar v)]])
             (Pretty.chunks (
               doublesemicolon [type_decl_p]
--- a/src/Tools/Code/code_preproc.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -306,7 +306,9 @@
     AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
     |> (map o apfst) (Code.string_of_const thy)
     |> sort (string_ord o apply2 fst)
-    |> map (fn (s, cert) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: Code.pretty_cert thy cert))
+    |> (map o apsnd) (Code.pretty_cert thy)
+    |> filter_out (null o snd)
+    |> map (fn (s, ps) => (Pretty.block o Pretty.fbreaks) (Pretty.str s :: ps))
     |> Pretty.chunks
   end;
 
--- a/src/Tools/Code/code_scala.ML	Thu Aug 03 13:35:28 2017 +0200
+++ b/src/Tools/Code/code_scala.ML	Fri Aug 04 18:03:50 2017 +0200
@@ -83,7 +83,6 @@
           let
             val (vs_tys, body) = Code_Thingol.unfold_abs t;
             val (ps, vars') = fold_map (print_abs_head tyvars) vs_tys vars;
-            val vars' = intro_vars (map_filter fst vs_tys) vars;
           in
             brackets (ps @| print_term tyvars false some_thm vars' NOBR body)
           end
@@ -183,22 +182,22 @@
       (fn (v, sort) => (Pretty.block o map str)
         (lookup_tyvar tyvars v :: maps (fn class => [" : ", deresolve_class class]) sort))
           NOBR (str s) vs;
-    fun print_defhead export tyvars vars const vs params tys ty =
+    fun print_defhead tyvars vars const vs params tys ty =
       concat [str "def", constraint (applify "(" ")" (fn (param, ty) =>
         constraint ((str o lookup_var vars) param) (print_typ tyvars NOBR ty))
           NOBR (print_context tyvars vs (deresolve_const const)) (params ~~ tys)) (print_typ tyvars NOBR ty),
             str "="];
-    fun print_def export const (vs, ty) [] =
+    fun print_def const (vs, ty) [] =
           let
             val (tys, ty') = Code_Thingol.unfold_fun ty;
             val params = Name.invent (snd reserved) "a" (length tys);
             val tyvars = intro_tyvars vs reserved;
             val vars = intro_vars params reserved;
           in
-            concat [print_defhead export tyvars vars const vs params tys ty',
+            concat [print_defhead tyvars vars const vs params tys ty',
               str ("sys.error(\"" ^ const ^ "\")")]
           end
-      | print_def export const (vs, ty) eqs =
+      | print_def const (vs, ty) eqs =
           let
             val tycos = fold (fn ((ts, t), _) =>
               fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
@@ -230,7 +229,7 @@
                   tuplify (map (print_term tyvars true some_thm vars' NOBR) ts),
                   str "=>", print_rhs vars' eq]
               end;
-            val head = print_defhead export tyvars vars2 const vs params tys' ty';
+            val head = print_defhead tyvars vars2 const vs params tys' ty';
           in if simple then
             concat [head, print_rhs vars2 (hd eqs)]
           else
@@ -269,9 +268,9 @@
           str "=", str "new", print_dicttyp tyvars classtyp, str "{"], str "}")
             (map print_classparam_instance (inst_params @ superinst_params))
       end;
-    fun print_stmt (Constant const, (export, Fun ((vs, ty), raw_eqs))) =
-          print_def export const (vs, ty) (filter (snd o snd) raw_eqs)
-      | print_stmt (Type_Constructor tyco, (export, Datatype (vs, cos))) =
+    fun print_stmt (Constant const, (_, Fun ((vs, ty), raw_eqs))) =
+          print_def const (vs, ty) (filter (snd o snd) raw_eqs)
+      | print_stmt (Type_Constructor tyco, (_, Datatype (vs, cos))) =
           let
             val tyvars = intro_tyvars (map (rpair []) vs) reserved;
             fun print_co ((co, vs_args), tys) =
@@ -288,7 +287,7 @@
               NOBR ((concat o map str) ["abstract", "sealed", "class", deresolve_tyco tyco]) vs
                 :: map print_co cos)
           end
-      | print_stmt (Type_Class class, (export, Class ((v, (classrels, classparams)), insts))) =
+      | print_stmt (Type_Class class, (_, Class ((v, (classrels, classparams)), insts))) =
           let
             val tyvars = intro_tyvars [(v, [class])] reserved;
             fun add_typarg s = Pretty.block