src/HOL/Hilbert_Choice.thy
changeset 12372 cd3a09c7dac9
parent 12298 b344486c33e2
child 13585 db4005b40cc6
equal deleted inserted replaced
12371:80ca9058db95 12372:cd3a09c7dac9
    35   Inv :: "'a set => ('a => 'b) => ('b => 'a)"
    35   Inv :: "'a set => ('a => 'b) => ('b => 'a)"
    36   "Inv A f == %x. SOME y. y : A & f y = x"
    36   "Inv A f == %x. SOME y. y : A & f y = x"
    37 
    37 
    38 
    38 
    39 use "Hilbert_Choice_lemmas.ML"
    39 use "Hilbert_Choice_lemmas.ML"
       
    40 declare someI_ex [elim?];
       
    41 
    40 
    42 
    41 lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    43 lemma tfl_some: "\<forall>P x. P x --> P (Eps P)"
    42   -- {* dynamically-scoped fact for TFL *}
    44   -- {* dynamically-scoped fact for TFL *}
    43   by (blast intro: someI)
    45   by (blast intro: someI)
    44 
    46