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/choice_specification.ML") |
10 uses ("Tools/meson.ML") |
|
11 ("Tools/choice_specification.ML") |
11 begin |
12 begin |
12 |
13 |
13 subsection {* Hilbert's epsilon *} |
14 subsection {* Hilbert's epsilon *} |
14 |
15 |
15 axiomatization Eps :: "('a => bool) => 'a" where |
16 axiomatization Eps :: "('a => bool) => 'a" where |