| changeset 715 | 3d7a9d4d2bb6 |
| parent 711 | 810d59a3d9b0 |
| child 719 | a9e55e1ef64c |
| 714:37f7dc85b61b | 715:3d7a9d4d2bb6 |
|---|---|
13 |
13 |
14 quotient int = "nat \<times> nat" / intrel |
14 quotient 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, minus, uminus, times, ord, abs, sgn}" |
18 instantiation int :: "{zero, one, plus, uminus, minus, times, ord, abs, sgn}" |
19 begin |
19 begin |
20 |
20 |
21 ML {* @{term "0 \<Colon> int"} *} |
21 ML {* @{term "0 \<Colon> int"} *} |
22 |
22 |
23 quotient_def |
23 quotient_def |