| changeset 1128 | 17ca92ab4660 |
| parent 998 | cfd2a42d60e3 |
| child 1139 | c4001cda9da3 |
| 1127:243a5ceaa088 | 1128:17ca92ab4660 |
|---|---|
1 theory IntEx |
1 theory IntEx |
2 imports "../QuotProd" "../QuotList" |
2 imports "../Quotient_Product" "../Quotient_List" |
3 begin |
3 begin |
4 |
4 |
5 fun |
5 fun |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
7 where |
7 where |