# HG changeset patch
# User paulson
# Date 935570741 -7200
# Node ID b275ae194e5a876186df0a27b577d4529d1d656a
# Parent  3f8eeb0b6d754aa0aef00c7c1b21d975306bc790
new theorem inv_f_eq

diff -r 3f8eeb0b6d75 -r b275ae194e5a src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Tue Aug 24 23:28:02 1999 +0200
+++ b/src/HOL/Fun.ML	Wed Aug 25 10:45:41 1999 +0200
@@ -117,8 +117,12 @@
 Goalw [inv_def] "inj(f) ==> inv f (f x) = x";
 by (etac inj_select 1);
 qed "inv_f_f";
+Addsimps [inv_f_f];
 
-Addsimps [inv_f_f];
+Goal "[| inj(f);  f x = y |] ==> inv f y = x";
+by (etac subst 1);
+by (etac inv_f_f 1);
+qed "inv_f_eq";
 
 (* Useful??? *)
 val [oneone,minor] = Goal