src/HOL/Library/Permutation.thy
changeset 44890 22f665a2e91c
parent 40122 1d8ad2ff3e01
child 50037 f2a32197a33a
     1.1 --- a/src/HOL/Library/Permutation.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Library/Permutation.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -153,7 +153,7 @@
     1.4  lemma perm_distinct_iff: "xs <~~> ys ==> distinct xs = distinct ys"
     1.5    apply (induct pred: perm)
     1.6       apply simp_all
     1.7 -   apply fastsimp
     1.8 +   apply fastforce
     1.9    apply (metis perm_set_eq)
    1.10    done
    1.11  
    1.12 @@ -171,7 +171,7 @@
    1.13      apply (metis Cons Cons_eq_appendI distinct.simps(2)
    1.14        distinct_remdups distinct_remdups_id perm_append_swap perm_distinct_iff)
    1.15     apply (subgoal_tac "set (a#list) = set (ysa@a#zs) & distinct (a#list) & distinct (ysa@a#zs)")
    1.16 -    apply (fastsimp simp add: insert_ident)
    1.17 +    apply (fastforce simp add: insert_ident)
    1.18     apply (metis distinct_remdups set_remdups)
    1.19     apply (subgoal_tac "length (remdups xs) < Suc (length xs)")
    1.20     apply simp