src/HOL/Library/Primes.thy
changeset 15131 c69542757a4d
parent 14706 71590b7733b7
child 15140 322485b816ac
equal deleted inserted replaced
15130:dc6be28d7f4e 15131:c69542757a4d
     4     Copyright   1996  University of Cambridge
     4     Copyright   1996  University of Cambridge
     5 *)
     5 *)
     6 
     6 
     7 header {* The Greatest Common Divisor and Euclid's algorithm *}
     7 header {* The Greatest Common Divisor and Euclid's algorithm *}
     8 
     8 
     9 theory Primes = Main:
     9 theory Primes
       
    10 import Main
       
    11 begin
    10 
    12 
    11 text {*
    13 text {*
    12   See \cite{davenport92}.
    14   See \cite{davenport92}.
    13   \bigskip
    15   \bigskip
    14 *}
    16 *}