--- 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);