equal
deleted
inserted
replaced
2 Author: Markus Wenzel, TU Muenchen |
2 Author: Markus Wenzel, TU Muenchen |
3 Author: Freek Wiedijk, Radboud University Nijmegen |
3 Author: Freek Wiedijk, Radboud University Nijmegen |
4 Author: Stefan Berghofer, TU Muenchen |
4 Author: Stefan Berghofer, TU Muenchen |
5 *) |
5 *) |
6 |
6 |
7 header {* Euclid's theorem *} |
7 section {* Euclid's theorem *} |
8 |
8 |
9 theory Euclid |
9 theory Euclid |
10 imports |
10 imports |
11 "~~/src/HOL/Number_Theory/UniqueFactorization" |
11 "~~/src/HOL/Number_Theory/UniqueFactorization" |
12 Util |
12 Util |