--- a/src/HOL/Combinatorics/Perm.thy Wed Oct 02 11:17:47 2024 +0200
+++ b/src/HOL/Combinatorics/Perm.thy Wed Oct 02 11:27:19 2024 +0200
@@ -794,16 +794,16 @@
bundle no_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)
+no_notation swap (\<open>\<langle>_ \<leftrightarrow> _\<rangle>\<close>)
+no_notation cycle (\<open>\<langle>_\<rangle>\<close>)
+no_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)
+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