--- a/src/Doc/Isar_Ref/Spec.thy Sat Nov 30 16:01:58 2024 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Sat Nov 30 16:42:22 2024 +0100
@@ -297,7 +297,9 @@
\<^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.
+ declaration inside a @{command bundle} definition: \<^verbatim>\<open>no\<close> means that
+ both the order and polarity of declarations is reversed (following
+ algebraic group laws).
Here is an artificial example of bundling various configuration options: