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