| changeset 504 | bb23a7393de3 |
| parent 494 | abafefa0d58b |
| child 505 | 6cdba30c6d66 |
| 503:d2c9a72e52e0 | 504:bb23a7393de3 |
|---|---|
1 theory IntEx |
1 theory IntEx |
2 imports QuotMain |
2 imports QuotMain |
3 begin |
3 begin |
4 |
|
4 |
5 |
5 fun |
6 fun |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
7 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
7 where |
8 where |
8 "intrel (x, y) (u, v) = (x + v = u + y)" |
9 "intrel (x, y) (u, v) = (x + v = u + y)" |