src/HOL/Hilbert_Choice.thy
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 *}