| changeset 33318 | ddd97d9dfbfb |
| parent 33197 | de6285ebcc05 |
| child 33657 | a4179bf442d1 |
| 33298:dfda74619509 | 33318:ddd97d9dfbfb |
|---|---|
26 |
26 |
27 |
27 |
28 header {* GCD *} |
28 header {* GCD *} |
29 |
29 |
30 theory GCD |
30 theory GCD |
31 imports Fact |
31 imports Fact Parity |
32 begin |
32 begin |
33 |
33 |
34 declare One_nat_def [simp del] |
34 declare One_nat_def [simp del] |
35 |
35 |
36 subsection {* gcd *} |
36 subsection {* gcd *} |