equal
deleted
inserted
replaced
5 |
5 |
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 Int = EquivClass + ArithSimp: |
10 theory Int imports EquivClass ArithSimp begin |
11 |
11 |
12 constdefs |
12 constdefs |
13 intrel :: i |
13 intrel :: i |
14 "intrel == {p : (nat*nat)*(nat*nat). |
14 "intrel == {p : (nat*nat)*(nat*nat). |
15 \<exists>x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}" |
15 \<exists>x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}" |