equal
deleted
inserted
replaced
9 |
9 |
10 text{*Allows quantification over any term having sort @{text logic}. Used to |
10 text{*Allows quantification over any term having sort @{text logic}. Used to |
11 quantify over classes. Yields a proposition rather than a FOL formula.*} |
11 quantify over classes. Yields a proposition rather than a FOL formula.*} |
12 |
12 |
13 constdefs |
13 constdefs |
14 ex :: "(('a::logic) => prop) => prop" (binder "?? " 0) |
14 ex :: "(('a::{}) => prop) => prop" (binder "?? " 0) |
15 "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)" |
15 "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)" |
16 |
16 |
17 syntax (xsymbols) |
17 syntax (xsymbols) |
18 "?? " :: "[idts, o] => o" ("(3\<Or>_./ _)" [0, 0] 0) |
18 "?? " :: "[idts, o] => o" ("(3\<Or>_./ _)" [0, 0] 0) |
19 |
19 |