--- 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>