# HG changeset patch
# User wenzelm
# Date 1728041373 -7200
# Node ID 6fefd6c602fa072c96a04b48b67751f9b34e8f3c
# Parent  d9e3161080f91bc8f00332c2a57f38ca8ad49ce5
clarified syntax for opening bundles;
updated and tuned documentation;

diff -r d9e3161080f9 -r 6fefd6c602fa NEWS
--- a/NEWS	Fri Oct 04 13:22:35 2024 +0200
+++ b/NEWS	Fri Oct 04 13:29:33 2024 +0200
@@ -13,6 +13,9 @@
 so its declarations are applied immediately, but also named for later
 re-use.
 
+* The syntax of opnening bundles has changed slightly: multiple bundles
+need to be separated by the keyword 'and'. Minor INCOMPATIBILITY.
+
 * Inner syntax translations now support formal dependencies via commands
 'syntax_types' or 'syntax_consts'. This is essentially an abstract
 specification of the effect of 'translations' (or translation functions
diff -r d9e3161080f9 -r 6fefd6c602fa src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri Oct 04 13:29:33 2024 +0200
@@ -211,10 +211,12 @@
   \begin{matharray}{rcl}
     @{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command "bundle"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
+    @{command_def "unbundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     @{command_def "include"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
     @{command_def "including"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
     @{keyword_def "includes"} & : & syntax \\
+    @{keyword_def "opening"} & : & syntax \\
   \end{matharray}
 
   The outer syntax of fact expressions (\secref{sec:syn-att}) involves
@@ -234,15 +236,17 @@
     (@@{command bundle} | @@{command open_bundle}) @{syntax name} \<newline>
       ( '=' @{syntax thms} @{syntax for_fixes} | @'begin')
     ;
+    @@{command unbundle} @{syntax bundles}
+    ;
     @@{command print_bundles} ('!'?)
     ;
-    (@@{command include} | @@{command including}) (@{syntax name}+)
+    (@@{command include} | @@{command including}) @{syntax bundles}
     ;
-    @{syntax_def "includes"}: @'includes' (@{syntax name}+)
+    @{syntax_def "includes"}: @'includes' @{syntax bundles}
     ;
-    @{syntax_def "opening"}: @'opening' (@{syntax name}+)
+    @{syntax_def "opening"}: @'opening' @{syntax bundles}
     ;
-    @@{command unbundle} (@{syntax name}+)
+    @{syntax bundles}: @{syntax name} + @'and'
   \<close>
 
   \<^descr> \<^theory_text>\<open>bundle b = decls\<close> defines a bundle of declarations in the current
@@ -259,32 +263,31 @@
   bindings are not recorded in the bundle.
 
   \<^descr> \<^theory_text>\<open>open_bundle b\<close> is like \<^theory_text>\<open>bundle b\<close> followed by \<^theory_text>\<open>unbundle b\<close>, so its
-  declarations are applied immediately, but also named for later re-use.
+  declarations are activated immediately, but also named for later re-use.
+
+  \<^descr> \<^theory_text>\<open>unbundle \<^vec>b\<close> activates the declarations from the given bundles in
+  the current local theory context. This is analogous to \<^theory_text>\<open>lemmas\<close>
+  (\secref{sec:theorems}) with the expanded bundles.
 
   \<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are available in the
   current context; the ``\<open>!\<close>'' option indicates extra verbosity.
 
-  \<^descr> \<^theory_text>\<open>include b\<^sub>1 \<dots> b\<^sub>n\<close> activates the declarations from the given bundles
-  in a proof body (forward mode). This is analogous to \<^theory_text>\<open>note\<close>
+  \<^descr> \<^theory_text>\<open>include \<^vec>b\<close> activates the declarations from the given bundles in a
+  proof body (forward mode). This is analogous to \<^theory_text>\<open>note\<close>
+  (\secref{sec:proof-facts}) with the expanded bundles.
+
+  \<^descr> \<^theory_text>\<open>including \<^vec>b\<close> is similar to \<^theory_text>\<open>include\<close>, but works in proof
+  refinement (backward mode). This is analogous to \<^theory_text>\<open>using\<close>
   (\secref{sec:proof-facts}) with the expanded bundles.
 
-  \<^descr> \<^theory_text>\<open>including b\<^sub>1 \<dots> b\<^sub>n\<close> is similar to \<^theory_text>\<open>include\<close>, but works in proof refinement
-  (backward mode). This is analogous to \<^theory_text>\<open>using\<close> (\secref{sec:proof-facts})
-  with the expanded bundles.
-
-  \<^descr> \<^theory_text>\<open>includes b\<^sub>1 \<dots> b\<^sub>n\<close> is similar to \<^theory_text>\<open>include\<close>, but applies to a
-  confined specification context: unnamed \<^theory_text>\<open>context\<close>s and
-  long statements of \<^theory_text>\<open>theorem\<close>.
+  \<^descr> \<^theory_text>\<open>includes \<^vec>b\<close> is similar to \<^theory_text>\<open>include\<close>, but applies to a confined
+  specification context: unnamed \<^theory_text>\<open>context\<close>s and long statements of
+  \<^theory_text>\<open>theorem\<close>.
 
-  \<^descr> \<^theory_text>\<open>opening b\<^sub>1 \<dots> b\<^sub>n\<close> is similar to \<^theory_text>\<open>includes\<close>, but applies to
-  a named specification context: \<^theory_text>\<open>locale\<close>s, \<^theory_text>\<open>class\<close>es and
-  named \<^theory_text>\<open>context\<close>s. The effect is confined to the surface context within the
-  specification block itself and the corresponding \<^theory_text>\<open>begin\<close> / \<^theory_text>\<open>end\<close> block.
-
-  \<^descr> \<^theory_text>\<open>unbundle b\<^sub>1 \<dots> b\<^sub>n\<close> activates the declarations from the given bundles in
-  the current local theory context. This is analogous to \<^theory_text>\<open>lemmas\<close>
-  (\secref{sec:theorems}) with the expanded bundles.
-
+  \<^descr> \<^theory_text>\<open>opening \<^vec>b\<close> is similar to \<^theory_text>\<open>includes\<close>, but applies to a named
+  specification context: \<^theory_text>\<open>locale\<close>s, \<^theory_text>\<open>class\<close>es and named \<^theory_text>\<open>context\<close>s. The
+  effect is confined to the surface context within the specification block
+  itself and the corresponding \<^theory_text>\<open>begin\<close> / \<^theory_text>\<open>end\<close> block.
 
   Here is an artificial example of bundling various configuration options:
 \<close>
diff -r d9e3161080f9 -r 6fefd6c602fa src/HOL/Library/Code_Target_Int.thy
--- a/src/HOL/Library/Code_Target_Int.thy	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Library/Code_Target_Int.thy	Fri Oct 04 13:29:33 2024 +0200
@@ -160,7 +160,7 @@
   by transfer (simp add: fun_eq_iff)
 
 context
-  includes integer.lifting bit_operations_syntax
+  includes integer.lifting and bit_operations_syntax
 begin
 
 declare [[code drop: \<open>bit :: int \<Rightarrow> _\<close> \<open>not :: int \<Rightarrow> _\<close>
diff -r d9e3161080f9 -r 6fefd6c602fa src/HOL/Library/Code_Target_Nat.thy
--- a/src/HOL/Library/Code_Target_Nat.thy	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Library/Code_Target_Nat.thy	Fri Oct 04 13:29:33 2024 +0200
@@ -11,7 +11,7 @@
 subsection \<open>Implementation for \<^typ>\<open>nat\<close>\<close>
 
 context
-includes natural.lifting integer.lifting
+includes natural.lifting and integer.lifting
 begin
 
 lift_definition Nat :: "integer \<Rightarrow> nat"
diff -r d9e3161080f9 -r 6fefd6c602fa src/HOL/Library/DAList.thy
--- a/src/HOL/Library/DAList.thy	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Library/DAList.thy	Fri Oct 04 13:29:33 2024 +0200
@@ -129,7 +129,7 @@
 subsection \<open>Quickcheck generators\<close>
 
 context
-  includes state_combinator_syntax term_syntax
+  includes state_combinator_syntax and term_syntax
 begin
 
 definition
diff -r d9e3161080f9 -r 6fefd6c602fa src/HOL/Library/Disjoint_FSets.thy
--- a/src/HOL/Library/Disjoint_FSets.thy	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Library/Disjoint_FSets.thy	Fri Oct 04 13:29:33 2024 +0200
@@ -62,7 +62,7 @@
 (* FIXME should be provable without lifting *)
 lemma fmadd_disjnt: "fdisjnt (fmdom m) (fmdom n) \<Longrightarrow> m ++\<^sub>f n = n ++\<^sub>f m"
 unfolding fdisjnt_alt_def
-including fset.lifting fmap.lifting
+including fset.lifting and fmap.lifting
 apply transfer
 apply (rule ext)
 apply (auto simp: map_add_def split: option.splits)
diff -r d9e3161080f9 -r 6fefd6c602fa src/HOL/Library/Finite_Map.thy
--- a/src/HOL/Library/Finite_Map.thy	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Library/Finite_Map.thy	Fri Oct 04 13:29:33 2024 +0200
@@ -1188,7 +1188,7 @@
 lemma fmap_exhaust[cases type: fmap]:
   obtains (fmempty) "m = fmempty"
         | (fmupd) x y m' where "m = fmupd x y m'" "x |\<notin>| fmdom m'"
-using that including fmap.lifting fset.lifting
+using that including fmap.lifting and fset.lifting
 proof transfer
   fix m P
   assume "finite (dom m)"
diff -r d9e3161080f9 -r 6fefd6c602fa src/HOL/Probability/PMF_Impl.thy
--- a/src/HOL/Probability/PMF_Impl.thy	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/Probability/PMF_Impl.thy	Fri Oct 04 13:29:33 2024 +0200
@@ -534,7 +534,7 @@
 begin
 
 context
-  includes state_combinator_syntax term_syntax
+  includes state_combinator_syntax and term_syntax
 begin
 
 definition
diff -r d9e3161080f9 -r 6fefd6c602fa src/HOL/String.thy
--- a/src/HOL/String.thy	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/HOL/String.thy	Fri Oct 04 13:29:33 2024 +0200
@@ -180,7 +180,7 @@
   by (auto simp add: UNIV_char_of_nat card_image)
 
 context
-  includes lifting_syntax integer.lifting natural.lifting
+  includes lifting_syntax and integer.lifting and natural.lifting
 begin
 
 lemma [transfer_rule]:
diff -r d9e3161080f9 -r 6fefd6c602fa src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Fri Oct 04 13:29:33 2024 +0200
@@ -17,6 +17,7 @@
   val specification:
     ((binding * string option * mixfix) list * Specification.multi_specs_cmd) parser
   val constdecl: (binding * string option * mixfix) parser
+  val bundles: (xstring * Position.T) list parser
   val includes: (xstring * Position.T) list parser
   val opening: (xstring * Position.T) list parser
   val locale_fixes: (binding * string option * mixfix) list parser
@@ -81,11 +82,16 @@
   >> Scan.triple2;
 
 
-(* locale and context elements *)
+(* bundles *)
+
+val bundles = Parse.and_list1 Parse.name_position;
 
-val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 Parse.name_position);
+val includes = Parse.$$$ "includes" |-- Parse.!!! bundles;
 
-val opening = Parse.$$$ "opening" |-- Parse.!!! (Scan.repeat1 Parse.name_position);
+val opening = Parse.$$$ "opening" |-- Parse.!!! bundles;
+
+
+(* locale and context elements *)
 
 val locale_fixes =
   Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix
diff -r d9e3161080f9 -r 6fefd6c602fa src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Oct 04 13:22:35 2024 +0200
+++ b/src/Pure/Pure.thy	Fri Oct 04 13:29:33 2024 +0200
@@ -654,18 +654,15 @@
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>unbundle\<close>
-    "open bundle in local theory"
-    (Scan.repeat1 Parse.name_position >> Bundle.unbundle_cmd);
+    "open bundle in local theory" (Parse_Spec.bundles >> Bundle.unbundle_cmd);
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>include\<close>
-    "open bundle in proof body"
-    (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.include_cmd));
+    "open bundle in proof body" (Parse_Spec.bundles >> (Toplevel.proof o Bundle.include_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>including\<close>
-    "open bundle in goal refinement"
-    (Scan.repeat1 Parse.name_position >> (Toplevel.proof o Bundle.including_cmd));
+    "open bundle in goal refinement" (Parse_Spec.bundles >> (Toplevel.proof o Bundle.including_cmd));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_bundles\<close>