| changeset 26748 | 4d51ddd6aa5c | 
| parent 26562 | 9d25ef112cf6 | 
| child 27760 | 3aa86edac080 | 
--- a/src/HOL/Hilbert_Choice.thy Thu Apr 24 16:53:04 2008 +0200 +++ b/src/HOL/Hilbert_Choice.thy Fri Apr 25 15:30:33 2008 +0200 @@ -7,7 +7,7 @@ header {* Hilbert's Epsilon-Operator and the Axiom of Choice *} theory Hilbert_Choice -imports Nat Wellfounded_Recursion +imports Nat Wellfounded uses ("Tools/meson.ML") ("Tools/specification_package.ML") begin