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