src/HOL/Hilbert_Choice.thy
changeset 13585 db4005b40cc6
parent 12372 cd3a09c7dac9
child 13763 f94b569cd610
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Sep 26 10:43:43 2002 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 26 10:51:29 2002 +0200
     1.3 @@ -39,6 +39,10 @@
     1.4  use "Hilbert_Choice_lemmas.ML"
     1.5  declare someI_ex [elim?];
     1.6  
     1.7 +lemma Inv_mem: "[| f ` A = B;  x \<in> B |] ==> Inv A f x \<in> A"
     1.8 +apply (unfold Inv_def)
     1.9 +apply (fast intro: someI2)
    1.10 +done
    1.11  
    1.12  lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    1.13    -- {* dynamically-scoped fact for TFL *}