equal
deleted
inserted
replaced
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 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 |
|
10 (*Rewrite the overloaded 0::int to (int 0)*) |
|
11 Addsimps [Zero_def]; |
9 |
12 |
10 (*** Proving that intrel is an equivalence relation ***) |
13 (*** Proving that intrel is an equivalence relation ***) |
11 |
14 |
12 val eqa::eqb::prems = goal Arith.thy |
15 val eqa::eqb::prems = goal Arith.thy |
13 "[| (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> \ |
16 "[| (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> \ |