equal
deleted
inserted
replaced
5 |
5 |
6 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *} |
6 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *} |
7 |
7 |
8 theory Hilbert_Choice |
8 theory Hilbert_Choice |
9 imports Nat Wellfounded Plain |
9 imports Nat Wellfounded Plain |
10 uses ("Tools/meson.ML") ("Tools/specification_package.ML") |
10 uses ("Tools/meson.ML") ("Tools/choice_specification.ML") |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Hilbert's epsilon *} |
13 subsection {* Hilbert's epsilon *} |
14 |
14 |
15 axiomatization Eps :: "('a => bool) => 'a" where |
15 axiomatization Eps :: "('a => bool) => 'a" where |
594 subsection {* Specification package -- Hilbertized version *} |
594 subsection {* Specification package -- Hilbertized version *} |
595 |
595 |
596 lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c" |
596 lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c" |
597 by (simp only: someI_ex) |
597 by (simp only: someI_ex) |
598 |
598 |
599 use "Tools/specification_package.ML" |
599 use "Tools/choice_specification.ML" |
600 |
600 |
601 |
601 |
602 end |
602 end |