src/HOL/Library/Permutation.thy
changeset 26316 9e9e67e33557
parent 26072 f65a7fa2da6c
child 27368 9f90ac19e32b
     1.1 --- a/src/HOL/Library/Permutation.thy	Tue Mar 18 20:33:29 2008 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Tue Mar 18 20:33:31 2008 +0100
     1.3 @@ -188,7 +188,7 @@
     1.4     apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
     1.5      apply (fastsimp simp add: insert_ident)
     1.6     apply (metis distinct_remdups set_remdups)
     1.7 -  apply (metis Nat.le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le)
     1.8 +  apply (metis le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le)
     1.9    done
    1.10  
    1.11  lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"