src/HOL/Combinatorics/Perm.thy
changeset 81106 849efff7de15
parent 81100 6ae3d0b2b8ad
child 81116 0fb1e2dd4122
--- a/src/HOL/Combinatorics/Perm.thy	Wed Oct 02 20:49:44 2024 +0200
+++ b/src/HOL/Combinatorics/Perm.thy	Wed Oct 02 22:08:52 2024 +0200
@@ -792,7 +792,7 @@
 
 subsection \<open>Syntax\<close>
 
-bundle no_permutation_syntax
+open_bundle no_permutation_syntax
 begin
 no_notation swap    (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
 no_notation cycle   (\<open>\<langle>_\<rangle>\<close>)
@@ -806,6 +806,4 @@
 notation "apply"    (infixl \<open>\<langle>$\<rangle>\<close> 999)
 end
 
-unbundle no_permutation_syntax
-
 end