equal
deleted
inserted
replaced
37 zadd_def |
37 zadd_def |
38 "z + w == |
38 "z + w == |
39 Abs_Integ(UN p1:Rep_Integ(z). UN p2:Rep_Integ(w). |
39 Abs_Integ(UN p1:Rep_Integ(z). UN p2:Rep_Integ(w). |
40 split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)" |
40 split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)" |
41 |
41 |
42 zdiff_def "z - w == z + -(w::int)" |
42 zdiff_def "z - (w::int) == z + (-w)" |
43 |
43 |
44 zless_def "z<w == neg(z - w)" |
44 zless_def "z<w == neg(z - w)" |
45 |
45 |
46 zle_def "z <= (w::int) == ~(w < z)" |
46 zle_def "z <= (w::int) == ~(w < z)" |
47 |
47 |