# HG changeset patch
# User nipkow
# Date 1256037642 -7200
# Node ID 85d7a096e63f44aa81173e592ebd9dc935d6b4a0
# Parent  5c29cc66a0299bcf8b754586c2dad63524779a82
added inv_def for compatibility as a lemma

diff -r 5c29cc66a029 -r 85d7a096e63f src/HOL/Hilbert_Choice.thy
--- 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)