| changeset 21243 | afffe1f72143 |
| parent 21020 | 9af9ceb16d58 |
| child 21999 | 0cf192e489e2 |
--- a/src/HOL/Hilbert_Choice.thy Wed Nov 08 11:23:09 2006 +0100 +++ b/src/HOL/Hilbert_Choice.thy Wed Nov 08 13:48:29 2006 +0100 @@ -7,7 +7,7 @@ header {* Hilbert's Epsilon-Operator and the Axiom of Choice *} theory Hilbert_Choice -imports NatArith +imports Nat uses ("Tools/meson.ML") ("Tools/specification_package.ML") begin