--- a/src/HOL/Hilbert_Choice.thy Wed Jul 16 12:09:41 2003 +0200
+++ b/src/HOL/Hilbert_Choice.thy Thu Jul 17 15:23:20 2003 +0200
@@ -7,7 +7,7 @@
header {* Hilbert's epsilon-operator and everything to do with the Axiom of Choice *}
theory Hilbert_Choice = NatArith
-files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
+files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML") ("Tools/specification_package.ML"):
subsection {* Hilbert's epsilon *}
@@ -268,4 +268,6 @@
use "Tools/meson.ML"
setup meson_setup
+use "Tools/specification_package.ML"
+
end