| changeset 600 | 5d932e7a856c |
| parent 597 | 8a1c8dc72b5c |
| child 601 | 81f40b8bde7b |
| child 602 | e56eeb9fedb3 |
| 599:1e07e38ed6c5 | 600:5d932e7a856c |
|---|---|
1 theory IntEx |
1 theory IntEx |
2 imports "../QuotMain" |
2 imports "../QuotList" |
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 |