src/HOL/Hilbert_Choice.thy
changeset 39036 dff91b90d74c
parent 35416 d8d7d1b785af
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Sep 02 11:02:13 2010 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 02 11:29:02 2010 +0200
     1.3 @@ -7,7 +7,8 @@
     1.4  
     1.5  theory Hilbert_Choice
     1.6  imports Nat Wellfounded Plain
     1.7 -uses ("Tools/meson.ML") ("Tools/choice_specification.ML")
     1.8 +uses ("Tools/meson.ML")
     1.9 +     ("Tools/choice_specification.ML")
    1.10  begin
    1.11  
    1.12  subsection {* Hilbert's epsilon *}