changeset 25762 | c03e9d04b3e4 |
parent 25571 | c9e39eafc7a0 |
25761:466e714de2fc | 25762:c03e9d04b3e4 |
---|---|
20 |
20 |
21 typedef (Integ) |
21 typedef (Integ) |
22 int = "UNIV//intrel" |
22 int = "UNIV//intrel" |
23 by (auto simp add: quotient_def) |
23 by (auto simp add: quotient_def) |
24 |
24 |
25 instantiation int :: "{zero, one, plus, minus, times, ord, abs, sgn}" |
25 instantiation int :: "{zero, one, plus, minus, uminus, times, ord, abs, sgn}" |
26 begin |
26 begin |
27 |
27 |
28 definition |
28 definition |
29 Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})" |
29 Zero_int_def [code func del]: "0 = Abs_Integ (intrel `` {(0, 0)})" |
30 |
30 |