equal
deleted
inserted
replaced
20 syntax (HOL) |
20 syntax (HOL) |
21 "_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) |
21 "_Eps" :: "[pttrn, bool] => 'a" ("(3@ _./ _)" [0, 10] 10) |
22 syntax |
22 syntax |
23 "_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10) |
23 "_Eps" :: "[pttrn, bool] => 'a" ("(3SOME _./ _)" [0, 10] 10) |
24 translations |
24 translations |
25 "SOME x. P" == "Eps (%x. P)" |
25 "SOME x. P" => "Eps (%x. P)" |
|
26 |
|
27 print_translation {* |
|
28 (* to avoid eta-contraction of body *) |
|
29 [("Eps", fn [Abs abs] => |
|
30 let val (x,t) = atomic_abs_tr' abs |
|
31 in Syntax.const "_Eps" $ x $ t end)] |
|
32 *} |
26 |
33 |
27 axioms |
34 axioms |
28 someI: "P (x::'a) ==> P (SOME x. P x)" |
35 someI: "P (x::'a) ==> P (SOME x. P x)" |
29 |
36 |
30 |
37 |