equal
deleted
inserted
replaced
8 fun |
8 fun |
9 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
9 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
10 where |
10 where |
11 "intrel (x, y) (u, v) = (x + v = u + y)" |
11 "intrel (x, y) (u, v) = (x + v = u + y)" |
12 |
12 |
13 quotient int = "nat \<times> nat" / intrel |
13 quotient_type int = "nat \<times> nat" / intrel |
14 by (auto simp add: equivp_def expand_fun_eq) |
14 by (auto simp add: equivp_def expand_fun_eq) |
15 |
15 |
16 instantiation int :: "{zero, one, plus, uminus, minus, times, ord}" |
16 instantiation int :: "{zero, one, plus, uminus, minus, times, ord}" |
17 begin |
17 begin |
18 |
18 |