equal
deleted
inserted
replaced
84 "P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & |
84 "P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & |
85 (x1,y1):Rep_REAL(P) & (x2,y2):Rep_REAL(Q)" |
85 (x1,y1):Rep_REAL(P) & (x2,y2):Rep_REAL(Q)" |
86 real_le_def |
86 real_le_def |
87 "P <= (Q::real) == ~(Q < P)" |
87 "P <= (Q::real) == ~(Q < P)" |
88 |
88 |
89 syntax (symbols) |
89 syntax (xsymbols) |
90 Reals :: "'a set" ("\\<real>") |
90 Reals :: "'a set" ("\\<real>") |
91 Nats :: "'a set" ("\\<nat>") |
91 Nats :: "'a set" ("\\<nat>") |
92 |
92 |
93 end |
93 end |