1.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Sep 29 00:58:54 2005 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Sep 29 00:58:55 2005 +0200
     1.3 @@ -34,6 +34,8 @@
     1.4  
     1.5  axioms
     1.6    someI: "P (x::'a) ==> P (SOME x. P x)"
     1.7 +finalconsts
     1.8 +  Eps
     1.9  
    1.10  
    1.11  constdefs