src/HOL/Hilbert_Choice.thy
changeset 14115 65ec3f73d00b
parent 13764 3e180bf68496
child 14208 144f45277d5a
equal deleted inserted replaced
14114:e97ca1034caa 14115:65ec3f73d00b
     5 *)
     5 *)
     6 
     6 
     7 header {* Hilbert's epsilon-operator and everything to do with the Axiom of Choice *}
     7 header {* Hilbert's epsilon-operator and everything to do with the Axiom of Choice *}
     8 
     8 
     9 theory Hilbert_Choice = NatArith
     9 theory Hilbert_Choice = NatArith
    10 files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML"):
    10 files ("Hilbert_Choice_lemmas.ML") ("meson_lemmas.ML") ("Tools/meson.ML") ("Tools/specification_package.ML"):
    11 
    11 
    12 
    12 
    13 subsection {* Hilbert's epsilon *}
    13 subsection {* Hilbert's epsilon *}
    14 
    14 
    15 consts
    15 consts
   266 
   266 
   267 use "meson_lemmas.ML"
   267 use "meson_lemmas.ML"
   268 use "Tools/meson.ML"
   268 use "Tools/meson.ML"
   269 setup meson_setup
   269 setup meson_setup
   270 
   270 
       
   271 use "Tools/specification_package.ML"
       
   272 
   271 end
   273 end