diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Doc/Isar_Ref/Spec.thy
--- 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>