| changeset 15131 | c69542757a4d |
| parent 14872 | 3f2144aebd76 |
| child 15140 | 322485b816ac |
--- a/src/HOL/Hilbert_Choice.thy Mon Aug 16 14:21:54 2004 +0200 +++ b/src/HOL/Hilbert_Choice.thy Mon Aug 16 14:22:27 2004 +0200 @@ -6,9 +6,10 @@ header {* Hilbert's Epsilon-Operator and the Axiom of Choice *} -theory Hilbert_Choice = NatArith -files ("Tools/meson.ML") ("Tools/specification_package.ML"): - +theory Hilbert_Choice +import NatArith +files ("Tools/meson.ML") ("Tools/specification_package.ML") +begin subsection {* Hilbert's epsilon *}