changeset 223 | e8f719547298 |
parent 171 | 16c4ea954511 |
--- a/Fun.ML Tue Feb 28 10:52:55 1995 +0100 +++ b/Fun.ML Wed Mar 01 13:26:50 1995 +0100 @@ -125,6 +125,10 @@ by (REPEAT (resolve_tac prems 1)); qed "inj_ontoD"; +goal Fun.thy "!!x y.[| inj_onto(f,A); x:A; y:A |] ==> (f(x)=f(y)) = (x=y)"; +by (fast_tac (HOL_cs addSEs [inj_ontoD]) 1); +qed "inj_onto_iff"; + val major::prems = goal Fun.thy "[| inj_onto(f,A); ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)"; by (rtac contrapos 1);