src/HOL/Hilbert_Choice.thy
changeset 31723 f5cafe803b55
parent 31454 2c0959ab073f
child 32988 d1d4d7a08a66
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Jun 18 18:31:14 2009 -0700
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Jun 19 17:23:21 2009 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  theory Hilbert_Choice
     1.6  imports Nat Wellfounded Plain
     1.7 -uses ("Tools/meson.ML") ("Tools/specification_package.ML")
     1.8 +uses ("Tools/meson.ML") ("Tools/choice_specification.ML")
     1.9  begin
    1.10  
    1.11  subsection {* Hilbert's epsilon *}
    1.12 @@ -596,7 +596,7 @@
    1.13  lemma exE_some: "[| Ex P ; c == Eps P |] ==> P c"
    1.14    by (simp only: someI_ex)
    1.15  
    1.16 -use "Tools/specification_package.ML"
    1.17 +use "Tools/choice_specification.ML"
    1.18  
    1.19  
    1.20  end