src/HOL/Hilbert_Choice.thy
changeset 14115 65ec3f73d00b
parent 13764 3e180bf68496
child 14208 144f45277d5a
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Jul 16 12:09:41 2003 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Jul 17 15:23:20 2003 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Hilbert's epsilon-operator and everything to do with the Axiom of Choice *}
     1.5  
     1.6  theory Hilbert_Choice = NatArith
     1.7 -files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
     1.8 +files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML") ("Tools/specification_package.ML"):
     1.9  
    1.10  
    1.11  subsection {* Hilbert's epsilon *}
    1.12 @@ -268,4 +268,6 @@
    1.13  use "Tools/meson.ML"
    1.14  setup meson_setup
    1.15  
    1.16 +use "Tools/specification_package.ML"
    1.17 +
    1.18  end