| changeset 15131 | c69542757a4d |
| parent 15013 | 34264f5e4691 |
| child 15140 | 322485b816ac |
| 15130:dc6be28d7f4e | 15131:c69542757a4d |
|---|---|
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Rational numbers *} |
6 header {* Rational numbers *} |
7 |
7 |
8 theory Rational = Quotient + Main |
8 theory Rational |
9 files ("rat_arith.ML"): |
9 import Quotient |
10 files ("rat_arith.ML") |
|
11 begin |
|
10 |
12 |
11 subsection {* Fractions *} |
13 subsection {* Fractions *} |
12 |
14 |
13 subsubsection {* The type of fractions *} |
15 subsubsection {* The type of fractions *} |
14 |
16 |