# HG changeset patch
# User haftmann
# Date 1604246089 -3600
# Node ID 589645894305cc88238afa86703b6387aae7899c
# Parent  7cb68b5b103dd32239c7d9a0a4d136825bf9e894
bundle mixins for locale and class specifications

diff -r 7cb68b5b103d -r 589645894305 src/Doc/Implementation/Local_Theory.thy
--- a/src/Doc/Implementation/Local_Theory.thy	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Doc/Implementation/Local_Theory.thy	Sun Nov 01 16:54:49 2020 +0100
@@ -91,7 +91,7 @@
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type local_theory: Proof.context} \\
-  @{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex]
+  @{index_ML Named_Target.init: "string list -> 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 ->
@@ -104,7 +104,7 @@
   context data. Subtyping means that any value \<open>lthy:\<close>~\<^ML_type>\<open>local_theory\<close>
   can be also used with operations on expecting a regular \<open>ctxt:\<close>~\<^ML_type>\<open>Proof.context\<close>.
 
-  \<^descr> \<^ML>\<open>Named_Target.init\<close>~\<open>before_exit name thy\<close> initializes a local theory
+  \<^descr> \<^ML>\<open>Named_Target.init\<close>~\<open>includes name thy\<close> initializes a local theory
   derived from the given background theory. An empty name refers to a \<^emph>\<open>global
   theory\<close> context, and a non-empty name refers to a @{command locale} or
   @{command class} context (a fully-qualified internal name is expected here).
diff -r 7cb68b5b103d -r 589645894305 src/HOL/Library/Perm.thy
--- a/src/HOL/Library/Perm.thy	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/HOL/Library/Perm.thy	Sun Nov 01 16:54:49 2020 +0100
@@ -730,7 +730,7 @@
 
 subsection \<open>Swaps\<close>
 
-lift_definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a perm"  ("\<langle>_\<leftrightarrow>_\<rangle>")
+lift_definition swap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a perm"  ("\<langle>_ \<leftrightarrow> _\<rangle>")
   is "\<lambda>a b. Fun.swap a b id"
 proof
   fix a b :: 'a
@@ -741,37 +741,37 @@
 qed simp
 
 lemma apply_swap_simp [simp]:
-  "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> a = b"
-  "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> b = a"
+  "\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> a = b"
+  "\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> b = a"
   by (transfer; simp)+
 
 lemma apply_swap_same [simp]:
-  "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> \<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = c"
+  "c \<noteq> a \<Longrightarrow> c \<noteq> b \<Longrightarrow> \<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c = c"
   by transfer simp
 
 lemma apply_swap_eq_iff [simp]:
-  "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = a \<longleftrightarrow> c = b"
-  "\<langle>a\<leftrightarrow>b\<rangle> \<langle>$\<rangle> c = b \<longleftrightarrow> c = a"
+  "\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c = a \<longleftrightarrow> c = b"
+  "\<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c = b \<longleftrightarrow> c = a"
   by (transfer; auto simp add: Fun.swap_def)+
 
 lemma swap_1 [simp]:
-  "\<langle>a\<leftrightarrow>a\<rangle> = 1"
+  "\<langle>a \<leftrightarrow> a\<rangle> = 1"
   by transfer simp
 
 lemma swap_sym:
-  "\<langle>b\<leftrightarrow>a\<rangle> = \<langle>a\<leftrightarrow>b\<rangle>"
+  "\<langle>b \<leftrightarrow> a\<rangle> = \<langle>a \<leftrightarrow> b\<rangle>"
   by (transfer; auto simp add: Fun.swap_def)+
 
 lemma swap_self [simp]:
-  "\<langle>a\<leftrightarrow>b\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> = 1"
+  "\<langle>a \<leftrightarrow> b\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> = 1"
   by transfer (simp add: Fun.swap_def fun_eq_iff)
 
 lemma affected_swap:
-  "a \<noteq> b \<Longrightarrow> affected \<langle>a\<leftrightarrow>b\<rangle> = {a, b}"
+  "a \<noteq> b \<Longrightarrow> affected \<langle>a \<leftrightarrow> b\<rangle> = {a, b}"
   by transfer (auto simp add: Fun.swap_def)
 
 lemma inverse_swap [simp]:
-  "inverse \<langle>a\<leftrightarrow>b\<rangle> = \<langle>a\<leftrightarrow>b\<rangle>"
+  "inverse \<langle>a \<leftrightarrow> b\<rangle> = \<langle>a \<leftrightarrow> b\<rangle>"
   by transfer (auto intro: inv_equality simp: Fun.swap_def)
 
 
@@ -793,14 +793,14 @@
 
 bundle no_permutation_syntax
 begin
-  no_notation swap    ("\<langle>_\<leftrightarrow>_\<rangle>")
+  no_notation swap    ("\<langle>_ \<leftrightarrow> _\<rangle>")
   no_notation cycle   ("\<langle>_\<rangle>")
   no_notation "apply" (infixl "\<langle>$\<rangle>" 999)
 end
 
 bundle permutation_syntax
 begin
-  notation swap       ("\<langle>_\<leftrightarrow>_\<rangle>")
+  notation swap       ("\<langle>_ \<leftrightarrow> _\<rangle>")
   notation cycle      ("\<langle>_\<rangle>")
   notation "apply"    (infixl "\<langle>$\<rangle>" 999)
 end
diff -r 7cb68b5b103d -r 589645894305 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/HOL/ROOT	Sun Nov 01 16:54:49 2020 +0100
@@ -681,6 +681,7 @@
     Simps_Case_Conv_Examples
     Sketch_and_Explore
     Sorting_Algorithms_Examples
+    Specifications_with_bundle_mixins
     Sqrt
     Sqrt_Script
     Sudoku
diff -r 7cb68b5b103d -r 589645894305 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/HOL/Statespace/state_space.ML	Sun Nov 01 16:54:49 2020 +0100
@@ -134,13 +134,13 @@
 
 fun add_locale name expr elems thy =
   thy
-  |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems
+  |> Expression.add_locale (Binding.name name) (Binding.name name) [] expr elems
   |> snd
   |> Local_Theory.exit;
 
 fun add_locale_cmd name expr elems thy =
   thy
-  |> Expression.add_locale_cmd (Binding.name name) Binding.empty (expression_no_pos expr) elems
+  |> Expression.add_locale_cmd (Binding.name name) Binding.empty [] (expression_no_pos expr) elems
   |> snd
   |> Local_Theory.exit;
 
@@ -298,7 +298,7 @@
 
 fun add_declaration name decl thy =
   thy
-  |> Named_Target.init name
+  |> Named_Target.init [] name
   |> (fn lthy => Local_Theory.declaration {syntax = true, pervasive = false} (decl lthy) lthy)
   |> Local_Theory.exit_global;
 
diff -r 7cb68b5b103d -r 589645894305 src/HOL/ex/Perm_Fragments.thy
--- a/src/HOL/ex/Perm_Fragments.thy	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/HOL/ex/Perm_Fragments.thy	Sun Nov 01 16:54:49 2020 +0100
@@ -6,13 +6,14 @@
 imports "HOL-Library.Perm" "HOL-Library.Dlist"
 begin
 
-unbundle permutation_syntax
-
-
 text \<open>On cycles\<close>
 
+context
+  includes permutation_syntax
+begin
+
 lemma cycle_prod_list:
-  "\<langle>a # as\<rangle> = prod_list (map (\<lambda>b. \<langle>a\<leftrightarrow>b\<rangle>) (rev as))"
+  "\<langle>a # as\<rangle> = prod_list (map (\<lambda>b. \<langle>a \<leftrightarrow> b\<rangle>) (rev as))"
   by (induct as) simp_all
 
 lemma cycle_append [simp]:
@@ -21,11 +22,11 @@
   case (3 b c as)
   then have "\<langle>a # (b # as) @ bs\<rangle> = \<langle>a # bs\<rangle> * \<langle>a # b # as\<rangle>"
     by simp
-  then have "\<langle>a # as @ bs\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> =
-    \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>"
+  then have "\<langle>a # as @ bs\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> =
+    \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a \<leftrightarrow> b\<rangle>"
     by (simp add: ac_simps)
-  then have "\<langle>a # as @ bs\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> =
-    \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>"
+  then have "\<langle>a # as @ bs\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> =
+    \<langle>a # bs\<rangle> * \<langle>a # as\<rangle> * \<langle>a \<leftrightarrow> b\<rangle> * \<langle>a \<leftrightarrow> b\<rangle>"
     by simp
   then have "\<langle>a # as @ bs\<rangle> = \<langle>a # bs\<rangle> * \<langle>a # as\<rangle>"
     by (simp add: ac_simps)
@@ -39,15 +40,15 @@
 proof (induct as rule: cycle.induct)
   case (3 a b as)
   from affected_times
-  have "affected (\<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>)
-    \<subseteq> affected \<langle>a # as\<rangle> \<union> affected \<langle>a\<leftrightarrow>b\<rangle>" .
+  have "affected (\<langle>a # as\<rangle> * \<langle>a \<leftrightarrow> b\<rangle>)
+    \<subseteq> affected \<langle>a # as\<rangle> \<union> affected \<langle>a \<leftrightarrow> b\<rangle>" .
   moreover from 3
   have "affected (\<langle>a # as\<rangle>) \<subseteq> insert a (set as)"
     by simp
   moreover
-  have "affected \<langle>a\<leftrightarrow>b\<rangle> \<subseteq> {a, b}"
+  have "affected \<langle>a \<leftrightarrow> b\<rangle> \<subseteq> {a, b}"
     by (cases "a = b") (simp_all add: affected_swap)
-  ultimately have "affected (\<langle>a # as\<rangle> * \<langle>a\<leftrightarrow>b\<rangle>)
+  ultimately have "affected (\<langle>a # as\<rangle> * \<langle>a \<leftrightarrow> b\<rangle>)
     \<subseteq> insert a (insert b (set as))"
     by blast
   then show ?case by auto
@@ -75,7 +76,7 @@
     case (snoc cs c)
     with distinct have "distinct (a # b # cs @ [c])"
       by simp
-    then have **: "\<langle>a\<leftrightarrow>b\<rangle> * \<langle>c\<leftrightarrow>a\<rangle> = \<langle>c\<leftrightarrow>a\<rangle> * \<langle>c\<leftrightarrow>b\<rangle>"
+    then have **: "\<langle>a \<leftrightarrow> b\<rangle> * \<langle>c \<leftrightarrow> a\<rangle> = \<langle>c \<leftrightarrow> a\<rangle> * \<langle>c \<leftrightarrow> b\<rangle>"
       by transfer (auto simp add: comp_def Fun.swap_def)
     with snoc * show ?thesis
       by (simp add: mult.assoc [symmetric])
@@ -109,7 +110,7 @@
 
 definition fixate :: "'a \<Rightarrow> 'a perm \<Rightarrow> 'a perm"
 where
-  "fixate a f = (if a \<in> affected f then f * \<langle>apply (inverse f) a\<leftrightarrow>a\<rangle> else f)"
+  "fixate a f = (if a \<in> affected f then f * \<langle>inverse f \<langle>$\<rangle> a \<leftrightarrow> a\<rangle> else f)"
 
 lemma affected_fixate_trivial:
   assumes "a \<notin> affected f"
@@ -258,6 +259,11 @@
 where
   "cycles f = map (\<lambda>a. trace a f) (seeds f)"
 
+end
+
+
+text \<open>Misc\<close>
+
 lemma (in comm_monoid_list_set) sorted_list_of_set:
   assumes "finite A"
   shows "list.F (map h (sorted_list_of_set A)) = set.F h A"
@@ -269,9 +275,6 @@
     by (simp)
 qed
 
-
-text \<open>Misc\<close>
-
 primrec subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
 where
   "subtract [] ys = ys"
diff -r 7cb68b5b103d -r 589645894305 src/HOL/ex/Specifications_with_bundle_mixins.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Specifications_with_bundle_mixins.thy	Sun Nov 01 16:54:49 2020 +0100
@@ -0,0 +1,60 @@
+theory Specifications_with_bundle_mixins
+  imports "HOL-Library.Perm"
+begin
+
+locale involutory =
+  includes permutation_syntax
+  fixes f :: \<open>'a perm\<close>
+  assumes involutory: \<open>\<And>x. f \<langle>$\<rangle> (f \<langle>$\<rangle> x) = x\<close>
+begin
+
+lemma
+  \<open>f * f = 1\<close>
+  using involutory
+  by (simp add: perm_eq_iff apply_sequence)
+
+end
+
+context involutory
+begin
+
+thm involutory (*syntax from permutation_syntax only present in locale specification and initial block*)
+
+end
+
+
+class at_most_two_elems =
+  includes permutation_syntax
+  assumes swap_distinct: \<open>a \<noteq> b \<Longrightarrow> \<langle>a \<leftrightarrow> b\<rangle> \<langle>$\<rangle> c \<noteq> c\<close>
+begin
+
+lemma
+  \<open>card (UNIV :: 'a set) \<le> 2\<close>
+proof (rule ccontr)
+  fix a :: 'a
+  assume \<open>\<not> card (UNIV :: 'a set) \<le> 2\<close>
+  then have c0: \<open>card (UNIV :: 'a set) \<ge> 3\<close>
+    by simp
+  then have [simp]: \<open>finite (UNIV :: 'a set)\<close>
+    using card.infinite by fastforce
+  from c0 card_Diff1_le [of UNIV a]
+  have ca: \<open>card (UNIV - {a}) \<ge> 2\<close>
+    by simp
+  then obtain b where \<open>b \<in> (UNIV - {a})\<close>
+    by (metis all_not_in_conv card.empty card_2_iff' le_zero_eq)
+  with ca card_Diff1_le [of \<open>UNIV - {a}\<close> b]
+  have cb: \<open>card (UNIV - {a, b}) \<ge> 1\<close> and \<open>a \<noteq> b\<close>
+    by simp_all
+  then obtain c where \<open>c \<in> (UNIV - {a, b})\<close>
+    by (metis One_nat_def all_not_in_conv card.empty le_zero_eq nat.simps(3))
+  then have \<open>a \<noteq> c\<close> \<open>b \<noteq> c\<close>
+    by auto
+  with swap_distinct [of a b c] show False
+    by (simp add: \<open>a \<noteq> b\<close>) 
+qed
+
+end
+
+thm swap_distinct (*syntax from permutation_syntax only present in class specification and initial block*)
+
+end
\ No newline at end of file
diff -r 7cb68b5b103d -r 589645894305 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Sun Nov 01 16:54:49 2020 +0100
@@ -6,9 +6,9 @@
 
 signature CLASS_DECLARATION =
 sig
-  val class: binding -> class list ->
+  val class: binding -> string list -> class list ->
     Element.context_i list -> theory -> string * local_theory
-  val class_cmd: binding -> xstring list ->
+  val class_cmd: binding -> (xstring * Position.T) list -> xstring list ->
     Element.context list -> theory -> string * local_theory
   val prove_subclass: tactic -> class ->
     local_theory -> local_theory
@@ -108,9 +108,10 @@
 
 (* reading and processing class specifications *)
 
-fun prep_class_elems prep_decl thy sups raw_elems =
+fun prep_class_elems prep_decl ctxt sups raw_elems =
   let
     (* user space type system: only permits 'a type variable, improves towards 'a *)
+    val thy = Proof_Context.theory_of ctxt;
     val algebra = Sign.classes_of thy;
     val inter_sort = curry (Sorts.inter_sort algebra);
     val proto_base_sort =
@@ -165,7 +166,7 @@
       #> Class.redeclare_operations thy sups
       #> Context.proof_map (Syntax_Phases.term_check 0 "singleton_fixate" (K singleton_fixate));
     val ((raw_supparams, _, raw_inferred_elems, _), _) =
-      Proof_Context.init_global thy
+      ctxt
       |> Context.proof_map (Syntax_Phases.term_check 0 "unify_params" (K unify_params))
       |> prep_decl raw_supexpr init_class_body raw_elems;
     fun filter_element (Element.Fixes []) = NONE
@@ -205,13 +206,13 @@
 val cert_class_elems = prep_class_elems Expression.cert_declaration;
 val read_class_elems = prep_class_elems Expression.cert_read_declaration;
 
-fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems =
+fun prep_class_spec prep_class prep_include prep_class_elems ctxt raw_supclasses raw_includes raw_elems =
   let
-    val thy_ctxt = Proof_Context.init_global thy;
+    val thy = Proof_Context.theory_of ctxt;
 
     (* prepare import *)
     val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
-    val sups = Sign.minimize_sort thy (map (prep_class thy_ctxt) raw_supclasses);
+    val sups = Sign.minimize_sort thy (map (prep_class ctxt) raw_supclasses);
     val _ =
       (case filter_out (Class.is_class thy) sups of
         [] => ()
@@ -225,11 +226,13 @@
       else ();
 
     (* infer types and base sort *)
-    val (base_sort, supparam_names, supexpr, inferred_elems) = prep_class_elems thy sups raw_elems;
+    val includes = map (prep_include ctxt) raw_includes;
+    val includes_ctxt = Bundle.includes includes ctxt;
+    val (base_sort, supparam_names, supexpr, inferred_elems) = prep_class_elems includes_ctxt sups raw_elems;
     val sup_sort = inter_sort base_sort sups;
 
     (* process elements as class specification *)
-    val class_ctxt = Class.begin sups base_sort thy_ctxt;
+    val class_ctxt = Class.begin sups base_sort includes_ctxt;
     val ((_, _, syntax_elems, _), _) = class_ctxt
       |> Expression.cert_declaration supexpr I inferred_elems;
     fun check_vars e vs =
@@ -250,10 +253,10 @@
       | fork_syn x = pair x;
     val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
 
-  in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end;
+  in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (includes, elems, global_syntax)) end;
 
-val cert_class_spec = prep_class_spec (K I) cert_class_elems;
-val read_class_spec = prep_class_spec Proof_Context.read_class read_class_elems;
+val cert_class_spec = prep_class_spec (K I) (K I) cert_class_elems;
+val read_class_spec = prep_class_spec Proof_Context.read_class Bundle.check read_class_elems;
 
 
 (* class establishment *)
@@ -313,15 +316,16 @@
       #> pair (param_map, params, assm_axiom)))
   end;
 
-fun gen_class prep_class_spec b raw_supclasses raw_elems thy =
+fun gen_class prep_class_spec b raw_includes raw_supclasses raw_elems thy =
   let
     val class = Sign.full_name thy b;
     val prefix = Binding.qualify true "class";
-    val (((sups, supparam_names), (supsort, base_sort, supexpr)), (elems, global_syntax)) =
-      prep_class_spec thy raw_supclasses raw_elems;
+    val ctxt = Proof_Context.init_global thy;
+    val (((sups, supparam_names), (supsort, base_sort, supexpr)), (includes, elems, global_syntax)) =
+      prep_class_spec ctxt raw_supclasses raw_includes raw_elems;
   in
     thy
-    |> Expression.add_locale b (prefix b) supexpr elems
+    |> Expression.add_locale b (prefix b) includes supexpr elems
     |> snd |> Local_Theory.exit_global
     |> adjungate_axclass b class base_sort sups supsort supparam_names global_syntax
     |-> (fn (param_map, params, assm_axiom) =>
@@ -334,7 +338,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 class
+    |> Named_Target.init includes class
     |> pair class
   end;
 
diff -r 7cb68b5b103d -r 589645894305 src/Pure/Isar/experiment.ML
--- a/src/Pure/Isar/experiment.ML	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/experiment.ML	Sun Nov 01 16:54:49 2020 +0100
@@ -29,7 +29,7 @@
     val experiment_name = Binding.name ("experiment" ^ serial_string ()) |> Binding.concealed;
     val lthy =
       thy
-      |> add_locale experiment_name Binding.empty ([], []) elems
+      |> add_locale experiment_name Binding.empty [] ([], []) elems
       |-> (Local_Theory.background_theory o Data.map o Symtab.insert_set);
     val (scope, naming) =
       Name_Space.new_scope (Proof_Context.naming_of (Local_Theory.target_of lthy));
diff -r 7cb68b5b103d -r 589645894305 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Nov 01 16:54:49 2020 +0100
@@ -32,9 +32,9 @@
   val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
     Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
-  val add_locale: binding -> binding ->
+  val add_locale: binding -> binding -> string list ->
     expression_i -> Element.context_i list -> theory -> string * local_theory
-  val add_locale_cmd: binding -> binding ->
+  val add_locale_cmd: binding -> binding -> (xstring * Position.T) list ->
     expression -> Element.context list -> theory -> string * local_theory
 
   (* Processing of locale expressions *)
@@ -796,15 +796,20 @@
 
 val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false;
 
-fun gen_add_locale prep_decl
-    binding raw_predicate_binding raw_import raw_body thy =
+fun gen_add_locale prep_include prep_decl
+    binding raw_predicate_binding raw_includes raw_import raw_body thy =
   let
     val name = Sign.full_name thy binding;
     val _ = Locale.defined thy name andalso
       error ("Duplicate definition of locale " ^ quote name);
 
+    val ctxt = Proof_Context.init_global thy;
+    val includes = map (prep_include ctxt) raw_includes;
+
     val ((fixed, deps, body_elems, _), (parms, ctxt')) =
-      prep_decl raw_import I raw_body (Proof_Context.init_global thy);
+      ctxt
+      |> Bundle.includes includes
+      |> prep_decl raw_import I raw_body;
     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
 
     val extraTs =
@@ -857,15 +862,15 @@
     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 name
+      |> Named_Target.init includes name
       |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
 
 in
 
-val add_locale = gen_add_locale cert_declaration;
-val add_locale_cmd = gen_add_locale read_declaration;
+val add_locale = gen_add_locale (K I) cert_declaration;
+val add_locale_cmd = gen_add_locale Bundle.check read_declaration;
 
 end;
 
diff -r 7cb68b5b103d -r 589645894305 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/interpretation.ML	Sun Nov 01 16:54:49 2020 +0100
@@ -191,7 +191,7 @@
 fun gen_global_sublocale prep_loc prep_interpretation
     raw_locale expression raw_defs thy =
   let
-    val lthy = Named_Target.init (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);
diff -r 7cb68b5b103d -r 589645894305 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/named_target.ML	Sun Nov 01 16:54:49 2020 +0100
@@ -11,7 +11,7 @@
   val locale_of: local_theory -> string option
   val bottom_locale_of: local_theory -> string option
   val class_of: local_theory -> string option
-  val init: string -> theory -> local_theory
+  val init: string list -> string -> theory -> local_theory
   val theory_init: theory -> local_theory
   val theory_map: (local_theory -> local_theory) -> theory -> theory
   val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->
@@ -115,24 +115,25 @@
   | setup_context (Locale locale) = Locale.init locale
   | setup_context (Class class) = Class.init class;
 
-fun init ident thy =
+fun init includes ident thy =
   let
     val target = target_of_ident thy ident;
   in
     thy
     |> Local_Theory.init
        {background_naming = Sign.naming_of thy |> Name_Space.mandatory_path (Long_Name.base_name ident),
-        setup = setup_context target #> Data.put (SOME target),
+        setup = setup_context target #> Data.put (SOME target) #> Bundle.includes includes,
         conclude = I}
        (operations target)
+    |> not (null includes) ? Local_Theory.mark_brittle
   end;
 
-val theory_init = init "";
+val theory_init = init [] "";
 
 fun theory_map g = theory_init #> g #> Local_Theory.exit_global;
 
 fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f;
 
-fun reinit lthy = init (ident_of lthy);
+fun reinit lthy = init [] (ident_of lthy);
 
 end;
diff -r 7cb68b5b103d -r 589645894305 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Sun Nov 01 16:54:49 2020 +0100
@@ -127,7 +127,10 @@
   Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
   Parse.$$$ "defines" || Parse.$$$ "notes";
 
-val class_expression = plus1_unless locale_keyword Parse.class;
+val locale_keyword' =
+  Parse.$$$ "includes" || locale_keyword;
+
+val class_expression = plus1_unless locale_keyword' Parse.class;
 
 val locale_expression =
   let
@@ -135,7 +138,7 @@
     val expr1 =
       locale_prefix -- expr2 --
       instance >> (fn ((p, l), i) => (l, (p, i)));
-    val expr0 = plus1_unless locale_keyword expr1;
+    val expr0 = plus1_unless locale_keyword' expr1;
   in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
 
 val context_element = Parse.group (fn () => "context element") loc_element;
diff -r 7cb68b5b103d -r 589645894305 src/Pure/Isar/target_context.ML
--- a/src/Pure/Isar/target_context.ML	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/target_context.ML	Sun Nov 01 16:54:49 2020 +0100
@@ -6,7 +6,8 @@
 
 signature TARGET_CONTEXT =
 sig
-  val context_begin_named_cmd: xstring * Position.T -> theory -> local_theory
+  val context_begin_named_cmd: (xstring * Position.T) list -> xstring * Position.T ->
+    theory -> local_theory
   val end_named_cmd: local_theory -> Context.generic
   val switch_named_cmd: (xstring * Position.T) option -> Context.generic ->
     (local_theory -> Context.generic) * local_theory
@@ -18,28 +19,33 @@
 structure Target_Context: TARGET_CONTEXT =
 struct
 
-fun context_begin_named_cmd ("-", _) thy = Named_Target.theory_init thy
-  | context_begin_named_cmd target thy = Named_Target.init (Locale.check thy target) thy;
+fun prep_includes thy =
+  map (Bundle.check (Proof_Context.init_global thy));
+
+fun context_begin_named_cmd raw_includes ("-", _) thy =
+      Named_Target.init (prep_includes thy raw_includes) "" thy
+  | context_begin_named_cmd raw_includes name thy =
+      Named_Target.init (prep_includes thy raw_includes) (Locale.check thy name) thy;
 
 val end_named_cmd = Context.Theory o Local_Theory.exit_global;
 
 fun switch_named_cmd NONE (Context.Theory thy) =
-      (Context.Theory o Local_Theory.exit_global, Named_Target.theory_init thy)
+      (end_named_cmd, Named_Target.theory_init thy)
   | switch_named_cmd (SOME name) (Context.Theory thy) =
-      (Context.Theory o Local_Theory.exit_global, context_begin_named_cmd name thy)
+      (end_named_cmd, context_begin_named_cmd [] name thy)
   | switch_named_cmd NONE (Context.Proof lthy) =
       (Context.Proof o Local_Theory.reset, lthy)
   | switch_named_cmd (SOME name) (Context.Proof lthy) =
       (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global,
-        (context_begin_named_cmd name o Local_Theory.exit_global_nonbrittle) lthy);
+        (context_begin_named_cmd [] name o Local_Theory.exit_global_nonbrittle) lthy);
 
-fun includes raw_incls lthy =
-  Bundle.includes (map (Bundle.check lthy) raw_incls) lthy;
+fun includes raw_includes lthy =
+  Bundle.includes (map (Bundle.check lthy) raw_includes) lthy;
 
-fun context_begin_nested_cmd raw_incls raw_elems gthy =
+fun context_begin_nested_cmd raw_includes raw_elems gthy =
   gthy
   |> Context.cases Named_Target.theory_init Local_Theory.assert
-  |> includes raw_incls
+  |> includes raw_includes
   |> Expression.read_declaration ([], []) I raw_elems
   |> (#4 o fst)
   |> Local_Theory.begin_nested
diff -r 7cb68b5b103d -r 589645894305 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Pure.thy	Sun Nov 01 16:54:49 2020 +0100
@@ -627,7 +627,7 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>context\<close> "begin local theory context"
     ((Parse.name_position
-        >> (fn name => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd name)) ||
+        >> (fn name => Toplevel.begin_main_target true (Target_Context.context_begin_named_cmd [] name)) ||
       Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
         >> (fn (incls, elems) => Toplevel.begin_nested_target (Target_Context.context_begin_nested_cmd incls elems)))
       --| Parse.begin);
@@ -646,18 +646,21 @@
 ML \<open>
 local
 
+val locale_context_elements =
+  Scan.optional Parse_Spec.includes [] -- Scan.repeat1 Parse_Spec.context_element;
+
 val locale_val =
   Parse_Spec.locale_expression --
-    Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
-  Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
+    Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! locale_context_elements) ([], []) ||
+  locale_context_elements >> pair ([], []);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>locale\<close> "define named specification context"
     (Parse.binding --
-      Scan.optional (\<^keyword>\<open>=\<close> |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
-      >> (fn ((name, (expr, elems)), begin) =>
+      Scan.optional (\<^keyword>\<open>=\<close> |-- Parse.!!! locale_val) (([], []), ([], [])) -- Parse.opt_begin
+      >> (fn ((name, (expr, (includes, elems))), begin) =>
           Toplevel.begin_main_target begin
-            (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
+            (Expression.add_locale_cmd name Binding.empty includes expr elems #> snd)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>experiment\<close> "open private specification context"
@@ -706,17 +709,20 @@
 ML \<open>
 local
 
+val class_context_elements =
+  Scan.optional Parse_Spec.includes [] -- Scan.repeat1 Parse_Spec.context_element;
+
 val class_val =
   Parse_Spec.class_expression --
-    Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
-  Scan.repeat1 Parse_Spec.context_element >> pair [];
+    Scan.optional (\<^keyword>\<open>+\<close> |-- Parse.!!! class_context_elements) ([], []) ||
+  class_context_elements >> pair [];
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>class\<close> "define type class"
-   (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) ([], []) -- Parse.opt_begin
-    >> (fn ((name, (supclasses, elems)), begin) =>
+   (Parse.binding -- Scan.optional (\<^keyword>\<open>=\<close> |-- class_val) ([], ([], [])) -- Parse.opt_begin
+    >> (fn ((name, (supclasses, (includes, elems))), begin) =>
         Toplevel.begin_main_target begin
-          (Class_Declaration.class_cmd name supclasses elems #> snd)));
+          (Class_Declaration.class_cmd name includes supclasses elems #> snd)));
 
 val _ =
   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>subclass\<close> "prove a subclass relation"
diff -r 7cb68b5b103d -r 589645894305 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/ROOT.ML	Sun Nov 01 16:54:49 2020 +0100
@@ -260,6 +260,7 @@
 (*local theories and targets*)
 ML_file "Isar/locale.ML";
 ML_file "Isar/generic_target.ML";
+ML_file "Isar/bundle.ML";
 ML_file "Isar/overloading.ML";
 ML_file "axclass.ML";
 ML_file "Isar/class.ML";
@@ -267,10 +268,8 @@
 ML_file "Isar/expression.ML";
 ML_file "Isar/interpretation.ML";
 ML_file "Isar/class_declaration.ML";
-ML_file "Isar/bundle.ML";
 ML_file "Isar/target_context.ML";
 ML_file "Isar/experiment.ML";
-
 ML_file "simplifier.ML";
 ML_file "Tools/plugin.ML";