| changeset 5143 | b94cd208f073 |
| parent 5137 | 60205b0de9b9 |
| child 5147 | 825877190618 |
--- a/src/ZF/Perm.ML Tue Jul 14 13:33:12 1998 +0200 +++ b/src/ZF/Perm.ML Wed Jul 15 10:15:13 1998 +0200 @@ -133,7 +133,7 @@ by (rtac (prem RS lam_mono) 1); qed "id_mono"; -Goalw [inj_def,id_def] "!!A B. A<=B ==> id(A): inj(A,B)"; +Goalw [inj_def,id_def] "A<=B ==> id(A): inj(A,B)"; by (REPEAT (ares_tac [CollectI,lam_type] 1)); by (etac subsetD 1 THEN assume_tac 1); by (Simp_tac 1);