src/HOL/Hilbert_Choice.thy

--- a/src/HOL/Hilbert_Choice.thy	Thu Sep 26 10:43:43 2002 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 26 10:51:29 2002 +0200
@@ -39,6 +39,10 @@
 use "Hilbert_Choice_lemmas.ML"
 declare someI_ex [elim?];
 
+lemma Inv_mem: "[| f ` A = B;  x \<in> B |] ==> Inv A f x \<in> A"
+apply (unfold Inv_def)
+apply (fast intro: someI2)
+done
 
 lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
   -- {* dynamically-scoped fact for TFL *}