equal
deleted
inserted
replaced
4 Copyright 1996 University of Cambridge |
4 Copyright 1996 University of Cambridge |
5 |
5 |
6 The integers as equivalence classes over nat*nat. |
6 The integers as equivalence classes over nat*nat. |
7 *) |
7 *) |
8 |
8 |
9 IntDef = Equiv + Arithmetic + |
9 IntDef = Equiv + NatArith + |
10 constdefs |
10 constdefs |
11 intrel :: "((nat * nat) * (nat * nat)) set" |
11 intrel :: "((nat * nat) * (nat * nat)) set" |
12 "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}" |
12 "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}" |
13 |
13 |
14 typedef (Integ) |
14 typedef (Integ) |