first-class support for "unbundle no foobar_syntax" -- avoid redundant "bundle no_foobar_syntax" definitions;

--- a/NEWS	Fri Oct 04 23:38:04 2024 +0200
+++ b/NEWS	Sat Oct 05 14:58:36 2024 +0200
@@ -9,12 +9,18 @@
 
 *** General ***
 
+* Command "unbundle b" and its variants like "context includes b" allow
+an optional name prefix with the reserved word "no": "unbundle no b"
+etc. This inverts the polarity of bundled declarations like 'notation'
+vs. 'no_notation', and thus avoids redundant bundle definitions like
+"foobar_syntax" vs. "no_foobar_syntax", because "no foobar_syntax" may
+be used instead. Consequently, the syntax for multiple bundle names has
+been changed slightly, demanding an explicit 'and' keyword. Minor
+INCOMPATIBILITY.
+
 * Command "open_bundle b" is like "bundle b" followed by "unbundle b",
 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.
+re-use: "unbundle no b" etc.
 
 * Inner syntax translations now support formal dependencies via commands
 'syntax_types' or 'syntax_consts'. This is essentially an abstract
@@ -53,11 +59,11 @@
 * Various declaration bundles support adhoc modification of notation,
 notably like this:
 
-  unbundle no_list_syntax
-  unbundle no_listcompr_syntax
-  unbundle no_rtrancl_syntax
-  unbundle no_trancl_syntax
-  unbundle no_reflcl_syntax
+  unbundle no list_syntax
+  unbundle no listcompr_syntax
+  unbundle no rtrancl_syntax
+  unbundle no trancl_syntax
+  unbundle no reflcl_syntax
 
 This is more robust than individual 'no_syntax' / 'no_notation'
 commands, which need to copy mixfix declarations from elsewhere and thus

--- a/src/Doc/Datatypes/Datatypes.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -453,7 +453,7 @@
 Incidentally, this is how the traditional syntax can be set up:
 \<close>
 (*<*)
-unbundle no_list_syntax
+unbundle no list_syntax
 (*>*)
     syntax "_list" :: "args \<Rightarrow> 'a list" (\<open>[(_)]\<close>)
 

--- a/src/Doc/Implementation/Local_Theory.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Doc/Implementation/Local_Theory.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -91,7 +91,7 @@
 text %mlref \<open>
   \begin{mldecls}
   @{define_ML_type local_theory = Proof.context} \\
-  @{define_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex]
+  @{define_ML Named_Target.init: "Bundle.name list -> string -> theory -> local_theory"} \\[1ex]
   @{define_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory"} \\
   @{define_ML Local_Theory.note: "Attrib.binding * thm list ->

--- a/src/Doc/Isar_Ref/Spec.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -246,7 +246,7 @@
     ;
     @{syntax_def "opening"}: @'opening' @{syntax bundles}
     ;
-    @{syntax bundles}: @{syntax name} + @'and'
+    @{syntax bundles}: ('no')? @{syntax name} + @'and'
   \<close>
 
   \<^descr> \<^theory_text>\<open>bundle b = decls\<close> defines a bundle of declarations in the current
@@ -289,6 +289,17 @@
   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> Bundle names may be prefixed by the reserved word \<^verbatim>\<open>no\<close> to indicate that
+  the polarity of certain declaration commands should be inverted, notably:
+
+    \<^item> @{command syntax} versus @{command no_syntax}
+    \<^item> @{command notation} versus @{command no_notation}
+    \<^item> @{command type_notation} versus @{command no_type_notation}
+
+  This also works recursively for the @{command unbundle} command as
+  declaration inside a @{command bundle} definition.
+
+
   Here is an artificial example of bundling various configuration options:
 \<close>
 

--- a/src/HOL/Analysis/Cross3.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Analysis/Cross3.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -10,7 +10,7 @@
   imports Determinants Cartesian_Euclidean_Space
 begin
 
-context includes no_set_product_syntax
+context includes no set_product_syntax
 begin \<comment>\<open>locally disable syntax for set product, to avoid warnings\<close>
 
 definition\<^marker>\<open>tag important\<close> cross3 :: "[real^3, real^3] \<Rightarrow> real^3"  (infixr \<open>\<times>\<close> 80)
@@ -24,14 +24,9 @@
 open_bundle cross3_syntax
 begin
 notation cross3 (infixr \<open>\<times>\<close> 80)
-unbundle no_set_product_syntax
+unbundle no set_product_syntax
 end
 
-bundle no_cross3_syntax
-begin
-no_notation cross3 (infixr \<open>\<times>\<close> 80)
-unbundle set_product_syntax
-end
 
 subsection\<open> Basic lemmas\<close>
 
@@ -221,7 +216,7 @@
   shows "\<lbrakk>continuous_on S f; continuous_on S g\<rbrakk> \<Longrightarrow> continuous_on S (\<lambda>x. (f x) \<times> (g x))"
   by (simp add: continuous_on_eq_continuous_within continuous_cross)
 
-unbundle no_cross3_syntax
+unbundle no cross3_syntax
 
 end
 

--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -25,11 +25,6 @@
 notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
 end
 
-bundle no_vec_syntax
-begin
-no_notation vec_nth (infixl \<open>$\<close> 90) and vec_lambda (binder \<open>\<chi>\<close> 10)
-end
-
 text \<open>
   Concrete syntax for \<open>('a, 'b) vec\<close>:
     \<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close>

--- a/src/HOL/Analysis/Inner_Product.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Analysis/Inner_Product.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -466,9 +466,4 @@
 notation inner (infix \<open>\<bullet>\<close> 70)
 end
 
-bundle no_inner_syntax
-begin
-no_notation inner (infix \<open>\<bullet>\<close> 70)
 end
-
-end

--- a/src/HOL/Analysis/Lipschitz.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Analysis/Lipschitz.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -17,11 +17,6 @@
 notation\<^marker>\<open>tag important\<close> lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
 end
 
-bundle no_lipschitz_syntax
-begin
-no_notation lipschitz_on (\<open>_-lipschitz'_on\<close> [1000])
-end
-
 lemma lipschitz_onI: "L-lipschitz_on X f"
   if "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> L * dist x y" "0 \<le> L"
   using that by (auto simp: lipschitz_on_def)

--- a/src/HOL/Combinatorics/Perm.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Combinatorics/Perm.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -792,18 +792,13 @@
 
 subsection \<open>Syntax\<close>
 
-open_bundle no_permutation_syntax
+bundle permutation_syntax
 begin
-no_notation swap    (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
-no_notation cycle   (\<open>\<langle>_\<rangle>\<close>)
-no_notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
+notation swap    (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
+notation cycle   (\<open>\<langle>_\<rangle>\<close>)
+notation "apply" (infixl \<open>\<langle>$\<rangle>\<close> 999)
 end
 
-bundle permutation_syntax
-begin
-notation swap       (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
-notation cycle      (\<open>\<langle>_\<rangle>\<close>)
-notation "apply"    (infixl \<open>\<langle>$\<rangle>\<close> 999)
-end
+unbundle no permutation_syntax
 
 end

--- a/src/HOL/Decision_Procs/Approximation.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -1145,7 +1145,6 @@
 
 bundle floatarith_syntax
 begin
-
 notation Add (\<open>Add\<close>)
 notation Minus (\<open>Minus\<close>)
 notation Mult (\<open>Mult\<close>)
@@ -1164,31 +1163,6 @@
 notation Floor (\<open>Floor\<close>)
 notation Var (\<open>Var\<close>)
 notation Num (\<open>Num\<close>)
-
-end
-
-bundle no_floatarith_syntax
-begin
-
-no_notation Add (\<open>Add\<close>)
-no_notation Minus (\<open>Minus\<close>)
-no_notation Mult (\<open>Mult\<close>)
-no_notation Inverse (\<open>Inverse\<close>)
-no_notation Cos (\<open>Cos\<close>)
-no_notation Arctan (\<open>Arctan\<close>)
-no_notation Abs (\<open>Abs\<close>)
-no_notation Max (\<open>Max\<close>)
-no_notation Min (\<open>Min\<close>)
-no_notation Pi (\<open>Pi\<close>)
-no_notation Sqrt (\<open>Sqrt\<close>)
-no_notation Exp (\<open>Exp\<close>)
-no_notation Powr (\<open>Powr\<close>)
-no_notation Ln (\<open>Ln\<close>)
-no_notation Power (\<open>Power\<close>)
-no_notation Floor (\<open>Floor\<close>)
-no_notation Var (\<open>Var\<close>)
-no_notation Num (\<open>Num\<close>)
-
 end
 
 hide_const (open)

--- a/src/HOL/Library/Option_ord.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Library/Option_ord.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -449,6 +449,6 @@
 
 instance option :: (complete_linorder) complete_linorder ..
 
-unbundle no_lattice_syntax
+unbundle no lattice_syntax
 
 end

--- a/src/HOL/List.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/List.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -51,9 +51,9 @@
   "[x, xs]" \<rightleftharpoons> "x#[xs]"
   "[x]" \<rightleftharpoons> "x#[]"
 
-bundle no_list_syntax
+bundle list_syntax
 begin
-no_syntax
+syntax
   "_list" :: "args \<Rightarrow> 'a list"  (\<open>(\<open>indent=1 notation=\<open>mixfix list enumeration\<close>\<close>[_])\<close>)
 end
 
@@ -457,9 +457,9 @@
 syntax (ASCII)
   "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  (\<open>_ <- _\<close>)
 
-bundle no_listcompr_syntax
+bundle listcompr_syntax
 begin
-no_syntax
+syntax
   "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  (\<open>[_ . __\<close>)
   "_lc_end" :: "lc_quals" (\<open>]\<close>)
 end

--- a/src/HOL/Main.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Main.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -69,8 +69,8 @@
 begin
 
 notation
-  bot (\<open>\<bottom>\<close>) and
-  top (\<open>\<top>\<close>) and
+  bot  (\<open>\<bottom>\<close>) and
+  top  (\<open>\<top>\<close>) and
   inf  (infixl \<open>\<sqinter>\<close> 70) and
   sup  (infixl \<open>\<squnion>\<close> 65) and
   Inf  (\<open>\<Sqinter> _\<close> [900] 900) and
@@ -84,25 +84,6 @@
 
 end
 
-bundle no_lattice_syntax
-begin
-
-no_notation
-  bot (\<open>\<bottom>\<close>) and
-  top (\<open>\<top>\<close>) and
-  inf  (infixl \<open>\<sqinter>\<close> 70) and
-  sup  (infixl \<open>\<squnion>\<close> 65) and
-  Inf  (\<open>\<Sqinter> _\<close> [900] 900) and
-  Sup  (\<open>\<Squnion> _\<close> [900] 900)
-
-no_syntax
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_./ _)\<close> [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Sqinter>\<close>\<close>\<Sqinter>_\<in>_./ _)\<close> [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_./ _)\<close> [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  (\<open>(\<open>indent=3 notation=\<open>binder \<Squnion>\<close>\<close>\<Squnion>_\<in>_./ _)\<close> [0, 0, 10] 10)
+unbundle no lattice_syntax
 
 end
-
-unbundle no_lattice_syntax
-
-end

--- a/src/HOL/Product_Type.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Product_Type.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -1008,11 +1008,6 @@
 notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
 end
 
-bundle no_set_product_syntax
-begin
-no_notation Product_Type.Times (infixr \<open>\<times>\<close> 80)
-end
-
 syntax
   "_Sigma" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set"
     (\<open>(\<open>indent=3 notation=\<open>binder SIGMA\<close>\<close>SIGMA _:_./ _)\<close> [0, 0, 10] 10)

--- a/src/HOL/Set.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Set.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -38,15 +38,6 @@
   not_member  (\<open>(\<open>notation=\<open>infix ~:\<close>\<close>_/ ~: _)\<close> [51, 51] 50)
 end
 
-bundle no_member_ASCII_syntax
-begin
-no_notation (ASCII)
-  member  (\<open>'(:')\<close>) and
-  member  (\<open>(\<open>notation=\<open>infix :\<close>\<close>_/ : _)\<close> [51, 51] 50) and
-  not_member  (\<open>'(~:')\<close>) and
-  not_member  (\<open>(\<open>notation=\<open>infix ~:\<close>\<close>_/ ~: _)\<close> [51, 51] 50)
-end
-
 
 text \<open>Set comprehensions\<close>
 

--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -272,7 +272,9 @@
               |> Lifting_Info.lookup_quot_thm_quotients lthy2 |> is_some
             val qty_code_dt_bundle_name = bundle_name_of_rep_isom_data rep_isom_data
             val rep_isom = mk_rep_isom_of_code_dt qty_ret code_dt |> the
-            val lthy3 = if quot_active then lthy2 else Bundle.includes [qty_code_dt_bundle_name] lthy2
+            val lthy3 =
+              if quot_active then lthy2
+              else Bundle.includes [(true, qty_code_dt_bundle_name)] lthy2
             fun qty_isom_of_rep_isom rep = domain_type (dest_Const_type rep)
             val qty_isom = qty_isom_of_rep_isom rep_isom
             val f'_var = (Binding.suffix_name "_aux" (fst var), NoSyn);

--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -959,7 +959,7 @@
 
 fun pointer_of_bundle_name bundle_name ctxt =
   let
-    val bundle = Bundle.read ctxt bundle_name
+    val bundle = Bundle.get ctxt (Bundle.check ctxt bundle_name)
     fun err () = error "The provided bundle is not a lifting bundle"
   in
     (case bundle of

--- a/src/HOL/Transitive_Closure.thy	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/HOL/Transitive_Closure.thy	Sat Oct 05 14:58:36 2024 +0200
@@ -64,32 +64,32 @@
   tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000) and
   reflclp  (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)
 
-bundle no_rtrancl_syntax
+bundle rtrancl_syntax
 begin
-no_notation
+notation
   rtrancl  (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_\<^sup>*)\<close> [1000] 999) and
   rtranclp  (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_\<^sup>*\<^sup>*)\<close> [1000] 1000)
-no_notation (ASCII)
+notation (ASCII)
   rtrancl  (\<open>(\<open>notation=\<open>postfix *\<close>\<close>_^*)\<close> [1000] 999) and
   rtranclp  (\<open>(\<open>notation=\<open>postfix **\<close>\<close>_^**)\<close> [1000] 1000)
 end
 
-bundle no_trancl_syntax
+bundle trancl_syntax
 begin
-no_notation
+notation
   trancl  (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_\<^sup>+)\<close> [1000] 999) and
   tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_\<^sup>+\<^sup>+)\<close> [1000] 1000)
-no_notation (ASCII)
+notation (ASCII)
   trancl  (\<open>(\<open>notation=\<open>postfix +\<close>\<close>_^+)\<close> [1000] 999) and
   tranclp  (\<open>(\<open>notation=\<open>postfix ++\<close>\<close>_^++)\<close> [1000] 1000)
 end
 
-bundle no_reflcl_syntax
+bundle reflcl_syntax
 begin
-no_notation
+notation
   reflcl  (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_\<^sup>=)\<close> [1000] 999) and
   reflclp  (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_\<^sup>=\<^sup>=)\<close> [1000] 1000)
-no_notation (ASCII)
+notation (ASCII)
   reflcl  (\<open>(\<open>notation=\<open>postfix =\<close>\<close>_^=)\<close> [1000] 999) and
   reflclp  (\<open>(\<open>notation=\<open>postfix ==\<close>\<close>_^==)\<close> [1000] 1000)
 end

--- a/src/Pure/Isar/bundle.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/Isar/bundle.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -6,21 +6,22 @@
 
 signature BUNDLE =
 sig
-  type name = string
+  type name = bool * string
+  type xname = (bool * Position.T) * (xstring * Position.T)
   val bundle_space: Context.generic -> Name_Space.T
   val check: Proof.context -> xstring * Position.T -> string
-  val get: Proof.context -> name -> Attrib.thms
-  val read: Proof.context -> xstring * Position.T -> Attrib.thms
+  val check_name: Proof.context -> xname -> name
+  val get: Proof.context -> string -> Attrib.thms
   val extern: Proof.context -> string -> xstring
   val print_bundles: bool -> Proof.context -> unit
   val unbundle: name list -> local_theory -> local_theory
-  val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory
+  val unbundle_cmd: xname list -> local_theory -> local_theory
   val includes: name list -> Proof.context -> Proof.context
-  val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
+  val includes_cmd: xname list -> Proof.context -> Proof.context
   val include_: name list -> Proof.state -> Proof.state
-  val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
+  val include_cmd: xname list -> Proof.state -> Proof.state
   val including: name list -> Proof.state -> Proof.state
-  val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state
+  val including_cmd: xname list -> Proof.state -> Proof.state
   val bundle: {open_bundle: bool} -> binding * Attrib.thms ->
     (binding * typ option * mixfix) list -> local_theory -> local_theory
   val bundle_cmd: {open_bundle: bool} -> binding * (Facts.ref * Token.src list) list ->
@@ -44,7 +45,8 @@
 
 (* bundles *)
 
-type name = string
+type name = bool * string;
+type xname = (bool * Position.T) * (xstring * Position.T);
 
 val get_all_generic = #1 o Data.get;
 val get_all = get_all_generic o Context.Proof;
@@ -53,11 +55,12 @@
 
 fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_all ctxt);
 
+fun check_name ctxt ((b: bool, pos), arg) =
+  (Context_Position.report ctxt pos Markup.quasi_keyword; (b, check ctxt arg));
+
 val get_global = Name_Space.get o get_all_generic o Context.Theory;
 val get = Name_Space.get o get_all_generic o Context.Proof;
 
-fun read ctxt = get ctxt o check ctxt;
-
 fun extern ctxt = Name_Space.extern ctxt (Name_Space.space_of_table (get_all ctxt));
 
 
@@ -109,11 +112,19 @@
 
 (** open bundles **)
 
-fun apply_bundle loc bundle ctxt =
-  let val notes = if loc then Local_Theory.notes else Attrib.local_notes "" in
+fun polarity_decls b =
+  [([Drule.dummy_thm],
+    [Attrib.internal \<^here> (K (Thm.declaration_attribute (K (Syntax.set_polarity_generic b))))])];
+
+fun apply_bundle loc (add, bundle) ctxt =
+  let
+    val notes = if loc then Local_Theory.notes else Attrib.local_notes "";
+    val add0 = Syntax.get_polarity ctxt;
+    val add1 = Syntax.effective_polarity ctxt add;
+  in
     ctxt
     |> Context_Position.set_visible false
-    |> notes [(Binding.empty_atts, bundle)] |> snd
+    |> notes [(Binding.empty_atts, polarity_decls add1 @ bundle @ polarity_decls add0)] |> snd
     |> Context_Position.restore_visible ctxt
   end;
 
@@ -122,8 +133,8 @@
 fun gen_unbundle loc prep args ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val bundle = maps (prep ctxt) args |> transfer_bundle thy;
-  in apply_bundle loc bundle ctxt end;
+    val bundles = map (prep ctxt #> apsnd (get ctxt #> transfer_bundle thy)) args;
+  in fold (apply_bundle loc) bundles ctxt end;
 
 fun gen_includes prep = gen_unbundle false prep;
 
@@ -135,17 +146,17 @@
 
 in
 
-val unbundle = gen_unbundle true get;
-val unbundle_cmd = gen_unbundle true read;
+val unbundle = gen_unbundle true (K I);
+val unbundle_cmd = gen_unbundle true check_name;
 
-val includes = gen_includes get;
-val includes_cmd = gen_includes read;
+val includes = gen_includes (K I);
+val includes_cmd = gen_includes check_name;
 
-val include_ = gen_include get;
-val include_cmd = gen_include read;
+val include_ = gen_include (K I);
+val include_cmd = gen_include check_name;
 
-val including = gen_including get;
-val including_cmd = gen_including read;
+val including = gen_including (K I);
+val including_cmd = gen_including check_name;
 
 end;
 
@@ -180,7 +191,7 @@
       (fn phi => fn context =>
         let val psi = Morphism.set_trim_context'' context phi
         in #2 (define_bundle (Morphism.binding psi binding, transform_bundle psi bundle) context) end)
-    |> open_bundle ? apply_bundle true bundle
+    |> open_bundle ? apply_bundle true (true, bundle)
   end;
 
 in

--- a/src/Pure/Isar/class_declaration.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -8,7 +8,7 @@
 sig
   val class: binding -> Bundle.name list -> class list ->
     Element.context_i list -> theory -> string * local_theory
-  val class_cmd: binding -> (xstring * Position.T) list -> xstring list ->
+  val class_cmd: binding -> Bundle.xname list -> xstring list ->
     Element.context list -> theory -> string * local_theory
   val prove_subclass: tactic -> class ->
     local_theory -> local_theory
@@ -263,7 +263,7 @@
   in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (includes, elems, global_syntax)) end;
 
 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;
+val read_class_spec = prep_class_spec Proof_Context.read_class Bundle.check_name read_class_elems;
 
 
 (* class establishment *)

--- a/src/Pure/Isar/expression.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/Isar/expression.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -34,7 +34,7 @@
       * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context)
   val add_locale: binding -> binding -> Bundle.name list ->
     expression_i -> Element.context_i list -> theory -> string * local_theory
-  val add_locale_cmd: binding -> binding -> (xstring * Position.T) list ->
+  val add_locale_cmd: binding -> binding -> Bundle.xname list ->
     expression -> Element.context list -> theory -> string * local_theory
 
   (* Processing of locale expressions *)
@@ -874,7 +874,7 @@
 in
 
 val add_locale = gen_add_locale (K I) cert_declaration;
-val add_locale_cmd = gen_add_locale Bundle.check read_declaration;
+val add_locale_cmd = gen_add_locale Bundle.check_name read_declaration;
 
 end;
 

--- a/src/Pure/Isar/parse_spec.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/Isar/parse_spec.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -17,9 +17,9 @@
   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 bundles: Bundle.xname list parser
+  val includes: Bundle.xname list parser
+  val opening: Bundle.xname list parser
   val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
   val class_expression: string list parser
@@ -84,7 +84,11 @@
 
 (* bundles *)
 
-val bundles = Parse.and_list1 Parse.name_position;
+val bundle_polarity =
+  Scan.optional (Parse.position (Parse.reserved "no") >> (pair false o snd))
+    (true, Position.none);
+
+val bundles = Parse.and_list1 (bundle_polarity -- Parse.name_position);
 
 val includes = Parse.$$$ "includes" |-- Parse.!!! bundles;
 

--- a/src/Pure/Isar/proof_context.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -1140,8 +1140,10 @@
   else error ("Unknown syntax const: " ^ quote c ^ Position.here pos);
 
 fun syntax add mode args ctxt =
-  let val args' = map (pair Local_Syntax.Const) args
-  in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add mode args') end;
+  let
+    val add' = Syntax.effective_polarity ctxt add;
+    val args' = map (pair Local_Syntax.Const) args;
+  in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add' mode args') end;
 
 fun generic_syntax add mode args =
   Context.mapping (Sign.syntax_global add mode args) (syntax add mode args);
@@ -1163,8 +1165,10 @@
   | const_syntax _ _ = NONE;
 
 fun gen_notation make_syntax add mode args ctxt =
-  ctxt |> map_syntax_idents
-    (Local_Syntax.update_modesyntax ctxt add mode (map_filter (make_syntax ctxt) args));
+  let
+    val add' = Syntax.effective_polarity ctxt add;
+    val args' = map_filter (make_syntax ctxt) args;
+  in ctxt |> map_syntax_idents (Local_Syntax.update_modesyntax ctxt add' mode args') end;
 
 in
 

--- a/src/Pure/Isar/specification.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/Isar/specification.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -56,19 +56,19 @@
     bool -> local_theory -> (string * thm list) list * local_theory
   val theorem: bool -> string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    string list -> Element.context_i list -> Element.statement_i ->
+    Bundle.name list -> Element.context_i list -> Element.statement_i ->
     bool -> local_theory -> Proof.state
   val theorem_cmd: bool -> string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    (xstring * Position.T) list -> Element.context list -> Element.statement ->
+    Bundle.xname list -> Element.context list -> Element.statement ->
     bool -> local_theory -> Proof.state
   val schematic_theorem: bool -> string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    string list -> Element.context_i list -> Element.statement_i ->
+    Bundle.name list -> Element.context_i list -> Element.statement_i ->
     bool -> local_theory -> Proof.state
   val schematic_theorem_cmd: bool -> string -> Method.text option ->
     (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
-    (xstring * Position.T) list -> Element.context list -> Element.statement ->
+    Bundle.xname list -> Element.context list -> Element.statement ->
     bool -> local_theory -> Proof.state
 end;
 

--- a/src/Pure/Isar/target_context.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/Isar/target_context.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -6,12 +6,12 @@
 
 signature TARGET_CONTEXT =
 sig
-  val context_begin_named_cmd: (xstring * Position.T) list -> xstring * Position.T ->
+  val context_begin_named_cmd: Bundle.xname 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
-  val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list ->
+  val context_begin_nested_cmd: Bundle.xname list -> Element.context list ->
     Context.generic -> local_theory
   val end_nested_cmd: local_theory -> Context.generic
 end;
@@ -20,7 +20,7 @@
 struct
 
 fun prep_includes thy =
-  map (Bundle.check (Proof_Context.init_global thy));
+  map (Bundle.check_name (Proof_Context.init_global thy));
 
 fun context_begin_named_cmd raw_includes ("-", _) thy =
       Named_Target.init (prep_includes thy raw_includes) "" thy
@@ -44,7 +44,7 @@
       end;
 
 fun includes raw_includes lthy =
-  Bundle.includes (map (Bundle.check lthy) raw_includes) lthy;
+  Bundle.includes (map (Bundle.check_name lthy) raw_includes) lthy;
 
 fun context_begin_nested_cmd raw_includes raw_elems gthy =
   gthy

--- a/src/Pure/Syntax/syntax.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -116,6 +116,10 @@
   val update_consts: Proof.context -> (string * string list) list -> syntax -> syntax
   val update_trrules: Proof.context -> Ast.ast trrule list -> syntax -> syntax
   val remove_trrules: Proof.context -> Ast.ast trrule list -> syntax -> syntax
+  val get_polarity: Proof.context -> bool
+  val set_polarity: bool -> Proof.context -> Proof.context
+  val set_polarity_generic: bool -> Context.generic -> Context.generic
+  val effective_polarity: Proof.context -> bool -> bool
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
@@ -708,6 +712,8 @@
 
 (** modify syntax **)
 
+(* updates *)
+
 fun update_trfuns ctxt = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns ctxt;
 
 fun update_type_gram ctxt add prmode decls =
@@ -723,6 +729,17 @@
 fun remove_trrules ctxt = remove_syntax mode_default o Syntax_Ext.syn_ext_rules ctxt o check_rules;
 
 
+(* polarity of declarations: true = add, false = del *)
+
+val polarity = Config.declare_bool ("polarity", Position.none) (K true);
+
+fun get_polarity ctxt = Config.get ctxt polarity;
+val set_polarity = Config.put polarity;
+val set_polarity_generic = Config.put_generic polarity;
+
+fun effective_polarity ctxt add = get_polarity ctxt = add;
+
+
 open Lexicon.Syntax;
 
 end;

--- a/src/Pure/sign.ML	Fri Oct 04 23:38:04 2024 +0200
+++ b/src/Pure/sign.ML	Sat Oct 05 14:58:36 2024 +0200
@@ -393,27 +393,32 @@
   in thy |> map_syn (Syntax.update_const_gram ctxt add (logical_types thy) mode (map prep args)) end;
 
 fun syntax_global add mode args thy =
-  syntax (Proof_Context.init_global thy) add mode args thy;
+  let
+    val thy_ctxt = Proof_Context.init_global thy;
+    val add' = Syntax.effective_polarity thy_ctxt add;
+  in syntax thy_ctxt add' mode args thy end;
 
 val syntax_deps = update_syn_global Syntax.update_consts;
 
 fun type_notation_global add mode args thy =
   let
     val thy_ctxt = Proof_Context.init_global thy;
+    val add' = Syntax.effective_polarity thy_ctxt add;
     fun type_syntax (Type (c, args), mx) =
           SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx)
       | type_syntax _ = NONE;
-  in map_syn (Syntax.update_type_gram thy_ctxt add mode (map_filter type_syntax args)) thy end;
+  in map_syn (Syntax.update_type_gram thy_ctxt add' mode (map_filter type_syntax args)) thy end;
 
 fun notation_global add mode args thy =
   let
     val thy_ctxt = Proof_Context.init_global thy;
+    val add' = Syntax.effective_polarity thy_ctxt add;
     fun const_syntax (Const (c, _), mx) =
           (case try (Consts.type_scheme (consts_of thy)) c of
             SOME T => SOME (Lexicon.mark_const c, T, mx)
           | NONE => NONE)
       | const_syntax _ = NONE;
-  in syntax thy_ctxt add mode (map_filter const_syntax args) thy end;
+  in syntax thy_ctxt add' mode (map_filter const_syntax args) thy end;
 
 
 (* add constants *)