# HG changeset patch # User haftmann # Date 1238152921 -3600 # Node ID 3e89ac3905b9b837249670d0a73985a087af34f1 # Parent 9e23e3ea7eddb6603edd576f21cf7dc477a0de6c tuned notoriously slow metis proof diff -r 9e23e3ea7edd -r 3e89ac3905b9 src/HOL/Library/Permutation.thy --- a/src/HOL/Library/Permutation.thy Fri Mar 27 10:12:55 2009 +0100 +++ b/src/HOL/Library/Permutation.thy Fri Mar 27 12:22:01 2009 +0100 @@ -188,7 +188,11 @@ apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)") apply (fastsimp simp add: insert_ident) apply (metis distinct_remdups set_remdups) - apply (metis le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le) + apply (subgoal_tac "length (remdups xs) < Suc (length xs)") + apply simp + apply (subgoal_tac "length (remdups xs) \ length xs") + apply simp + apply (rule length_remdups_leq) done lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"