equal
deleted
inserted
replaced
5 Integers based on Quotients, based on an older version by Larry |
5 Integers based on Quotients, based on an older version by Larry |
6 Paulson. |
6 Paulson. |
7 *) |
7 *) |
8 |
8 |
9 theory Quotient_Int |
9 theory Quotient_Int |
10 imports "HOL-Library.Quotient_Product" HOL.Nat |
10 imports "HOL-Library.Quotient_Product" |
11 begin |
11 begin |
12 |
12 |
13 fun |
13 fun |
14 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
14 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
15 where |
15 where |