src/HOL/Library/Permutation.thy
changeset 69597 ff784d5a5bfb
parent 64587 8355a6e2df79
child 70680 b8cd7ea34e33
--- a/src/HOL/Library/Permutation.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Library/Permutation.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -8,7 +8,7 @@
 imports Multiset
 begin
 
-inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  ("_ <~~> _"  [50, 50] 50)  (* FIXME proper infix, without ambiguity!? *)
+inductive perm :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (\<open>_ <~~> _\<close>  [50, 50] 50)  (* FIXME proper infix, without ambiguity!? *)
 where
   Nil [intro!]: "[] <~~> []"
 | swap [intro!]: "y # x # l <~~> x # y # l"