| changeset 58889 | 5b7a9633cfa8 |
| parent 58834 | 773b378d9313 |
| child 59008 | f61482b0f240 |
| 58888:9537bf1c4853 | 58889:5b7a9633cfa8 |
|---|---|
23 |
23 |
24 Tobias Nipkow cleaned up a lot. |
24 Tobias Nipkow cleaned up a lot. |
25 *) |
25 *) |
26 |
26 |
27 |
27 |
28 header {* Greatest common divisor and least common multiple *} |
28 section {* Greatest common divisor and least common multiple *} |
29 |
29 |
30 theory GCD |
30 theory GCD |
31 imports Fact |
31 imports Fact |
32 begin |
32 begin |
33 |
33 |