| changeset 766 | df053507edba |
| parent 719 | a9e55e1ef64c |
| child 767 | 37285ec4387d |
| 765:d0250d01782c | 766:df053507edba |
|---|---|
9 fun |
9 fun |
10 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
10 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50) |
11 where |
11 where |
12 "intrel (x, y) (u, v) = (x + v = u + y)" |
12 "intrel (x, y) (u, v) = (x + v = u + y)" |
13 |
13 |
14 quotient int = "nat \<times> nat" / intrel |
14 quotient_type int = "nat \<times> nat" / intrel |
15 unfolding equivp_def |
15 unfolding equivp_def |
16 by (auto simp add: mem_def expand_fun_eq) |
16 by (auto simp add: mem_def expand_fun_eq) |
17 |
17 |
18 instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}" |
18 instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}" |
19 begin |
19 begin |