src/HOL/Library/Permutations.thy
changeset 33057 764547b68538
parent 32989 c28279b29ff1
child 33715 8cce3a34c122
     1.1 --- a/src/HOL/Library/Permutations.thy	Wed Oct 21 17:34:35 2009 +0200
     1.2 +++ b/src/HOL/Library/Permutations.thy	Thu Oct 22 09:27:48 2009 +0200
     1.3 @@ -83,7 +83,7 @@
     1.4    unfolding permutes_def by simp
     1.5  
     1.6  lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
     1.7 -  unfolding permutes_def inv_onto_def apply auto
     1.8 +  unfolding permutes_def inv_def apply auto
     1.9    apply (erule allE[where x=y])
    1.10    apply (erule allE[where x=y])
    1.11    apply (rule someI_ex) apply blast