added inv_def for compatibility as a lemma

--- a/src/HOL/Hilbert_Choice.thy	Tue Oct 20 11:36:19 2009 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Tue Oct 20 13:20:42 2009 +0200
@@ -91,6 +91,9 @@
 
 subsection {*Function Inverse*}
 
+lemma inv_def: "inv f = (%y. SOME x. f x = y)"
+by(simp add: inv_onto_def)
+
 lemma inv_onto_into: "x : f ` A ==> inv_onto A f x : A"
 apply (simp add: inv_onto_def)
 apply (fast intro: someI2)