tuned notoriously slow metis proof
authorhaftmann
Fri Mar 27 12:22:01 2009 +0100 (2009-03-27)
changeset 307423e89ac3905b9
parent 30741 9e23e3ea7edd
child 30743 2c83f7eaf1a4
tuned notoriously slow metis proof
src/HOL/Library/Permutation.thy
     1.1 --- a/src/HOL/Library/Permutation.thy	Fri Mar 27 10:12:55 2009 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Fri Mar 27 12:22:01 2009 +0100
     1.3 @@ -188,7 +188,11 @@
     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 le_less_trans Suc_length_conv length_remdups_leq less_Suc_eq nat_less_le)
     1.8 +   apply (subgoal_tac "length (remdups xs) < Suc (length xs)")
     1.9 +   apply simp
    1.10 +   apply (subgoal_tac "length (remdups xs) \<le> length xs")
    1.11 +   apply simp
    1.12 +   apply (rule length_remdups_leq)
    1.13    done
    1.14  
    1.15  lemma perm_remdups_iff_eq_set: "remdups x <~~> remdups y = (set x = set y)"