src/HOL/Hilbert_Choice.thy
changeset 13763 f94b569cd610
parent 13585 db4005b40cc6
child 13764 3e180bf68496
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sun Dec 22 10:42:09 2002 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sun Dec 22 10:43:43 2002 +0100
     1.3 @@ -22,7 +22,14 @@
     1.4  syntax
     1.5    "_Eps"        :: "[pttrn, bool] => 'a"    ("(3SOME _./ _)" [0, 10] 10)
     1.6  translations
     1.7 -  "SOME x. P" == "Eps (%x. P)"
     1.8 +  "SOME x. P" => "Eps (%x. P)"
     1.9 +
    1.10 +print_translation {*
    1.11 +(* to avoid eta-contraction of body *)
    1.12 +[("Eps", fn [Abs abs] =>
    1.13 +     let val (x,t) = atomic_abs_tr' abs
    1.14 +     in Syntax.const "_Eps" $ x $ t end)]
    1.15 +*}
    1.16  
    1.17  axioms
    1.18    someI: "P (x::'a) ==> P (SOME x. P x)"