equal
deleted
inserted
replaced
15 axiomatization Eps :: "('a => bool) => 'a" where |
15 axiomatization Eps :: "('a => bool) => 'a" where |
16 someI: "P x ==> P (Eps P)" |
16 someI: "P x ==> P (Eps P)" |
17 |
17 |
18 syntax (epsilon) |
18 syntax (epsilon) |
19 "_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) |
19 "_Eps" :: "[pttrn, bool] => 'a" ("(3\<some>_./ _)" [0, 10] 10) |
20 syntax (HOL) |
20 syntax (input) |
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" == "CONST Eps (%x. P)" |
25 "SOME x. P" == "CONST Eps (%x. P)" |