equal
deleted
inserted
replaced
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 |