equal
deleted
inserted
replaced
1 (* Title: HOL/Proofs/Extraction/Greatest_Common_Divisor.thy |
1 (* Title: HOL/Proofs/Extraction/Greatest_Common_Divisor.thy |
2 Author: Stefan Berghofer, TU Muenchen |
2 Author: Stefan Berghofer, TU Muenchen |
3 Author: Helmut Schwichtenberg, LMU Muenchen |
3 Author: Helmut Schwichtenberg, LMU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Greatest common divisor *} |
6 section {* Greatest common divisor *} |
7 |
7 |
8 theory Greatest_Common_Divisor |
8 theory Greatest_Common_Divisor |
9 imports QuotRem |
9 imports QuotRem |
10 begin |
10 begin |
11 |
11 |