| changeset 3842 | b55686a7b22c |
| parent 3341 | 89fe22bf9f54 |
| child 4059 | 59c1422c9da5 |
--- a/src/HOL/Fun.ML Fri Oct 10 18:37:49 1997 +0200 +++ b/src/HOL/Fun.ML Fri Oct 10 19:02:28 1997 +0200 @@ -46,7 +46,7 @@ by (etac arg_cong 1); qed "inj_eq"; -val [major] = goal Fun.thy "inj(f) ==> (@x.f(x)=f(y)) = y"; +val [major] = goal Fun.thy "inj(f) ==> (@x. f(x)=f(y)) = y"; by (rtac (major RS injD) 1); by (rtac selectI 1); by (rtac refl 1);