| changeset 25762 | c03e9d04b3e4 |
| parent 25571 | c9e39eafc7a0 |
| child 25885 | 6fbc3f54f819 |
| 25761:466e714de2fc | 25762:c03e9d04b3e4 |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Rational numbers *} |
6 header {* Rational numbers *} |
7 |
7 |
8 theory Rational |
8 theory Rational |
9 imports Abstract_Rat |
9 imports "~~/src/HOL/Library/Abstract_Rat" |
10 uses ("rat_arith.ML") |
10 uses ("rat_arith.ML") |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Rational numbers *} |
13 subsection {* Rational numbers *} |
14 |
14 |
161 lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel] |
161 lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel] |
162 |
162 |
163 |
163 |
164 subsubsection {* Standard operations on rational numbers *} |
164 subsubsection {* Standard operations on rational numbers *} |
165 |
165 |
166 instantiation rat :: "{zero, one, plus, minus, times, inverse, ord, abs, sgn}" |
166 instantiation rat :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}" |
167 begin |
167 begin |
168 |
168 |
169 definition |
169 definition |
170 Zero_rat_def [code func del]: "0 = Fract 0 1" |
170 Zero_rat_def [code func del]: "0 = Fract 0 1" |
171 |
171 |