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