changeset 28313 | 1742947952f8 |
parent 28091 | 50f2d6ba024c |
child 28351 | abfc66969d1f |
28312:f0838044f034 | 28313:1742947952f8 |
---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* Rational numbers *} |
6 header {* Rational numbers *} |
7 |
7 |
8 theory Rational |
8 theory Rational |
9 imports "../Nat_Int_Bij" GCD |
9 imports "../Nat_Int_Bij" "~~/src/HOL/Library/GCD" |
10 uses ("rat_arith.ML") |
10 uses ("rat_arith.ML") |
11 begin |
11 begin |
12 |
12 |
13 subsection {* Rational numbers as quotient *} |
13 subsection {* Rational numbers as quotient *} |
14 |
14 |