equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} |
8 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*} |
9 |
9 |
10 theory IntDef |
10 theory IntDef |
11 import Equiv NatArith |
11 imports Equiv NatArith |
12 begin |
12 begin |
13 |
13 |
14 constdefs |
14 constdefs |
15 intrel :: "((nat * nat) * (nat * nat)) set" |
15 intrel :: "((nat * nat) * (nat * nat)) set" |
16 --{*the equivalence relation underlying the integers*} |
16 --{*the equivalence relation underlying the integers*} |