src/HOL/Library/Perm.thy

 qed
 
 setup_lifting type_definition_perm
 
 notation "apply" (infixl "\<langle>$\<rangle>" 999)
-no_notation "apply" ("(\<langle>$\<rangle>)")
 
 lemma bij_apply [simp]:
   "bij (apply f)"
   using "apply" [of f] by simp
 

 bundle permutation_syntax
 begin
   notation swap       ("\<langle>_\<leftrightarrow>_\<rangle>")
   notation cycle      ("\<langle>_\<rangle>")
   notation "apply"    (infixl "\<langle>$\<rangle>" 999)
-  no_notation "apply" ("(\<langle>$\<rangle>)")
 end
 
 unbundle no_permutation_syntax
 
 end