equal
deleted
inserted
replaced
6 |
6 |
7 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *} |
7 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *} |
8 |
8 |
9 theory Hilbert_Choice |
9 theory Hilbert_Choice |
10 imports NatArith |
10 imports NatArith |
11 files ("Tools/meson.ML") ("Tools/specification_package.ML") |
11 uses ("Tools/meson.ML") ("Tools/specification_package.ML") |
12 begin |
12 begin |
13 |
13 |
14 subsection {* Hilbert's epsilon *} |
14 subsection {* Hilbert's epsilon *} |
15 |
15 |
16 consts |
16 consts |