--- a/src/HOL/Hilbert_Choice.thy Thu Sep 29 00:58:54 2005 +0200 +++ b/src/HOL/Hilbert_Choice.thy Thu Sep 29 00:58:55 2005 +0200 @@ -34,6 +34,8 @@ axioms someI: "P (x::'a) ==> P (SOME x. P x)" +finalconsts + Eps constdefs