src/HOL/Number_Theory/Cong.thy
changeset 58623 2db1df2c8467
parent 57512 cc97b347b301
child 58860 fee7cfa69c50
equal deleted inserted replaced
58622:aa99568f56de 58623:2db1df2c8467
     6 integers.
     6 integers.
     7 
     7 
     8 This file combines and revises a number of prior developments.
     8 This file combines and revises a number of prior developments.
     9 
     9 
    10 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    10 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    11 and Lawrence C. Paulson, based on \cite{davenport92}. They introduced
    11 and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
    12 gcd, lcm, and prime for the natural numbers.
    12 gcd, lcm, and prime for the natural numbers.
    13 
    13 
    14 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    14 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    15 extended gcd, lcm, primes to the integers. Amine Chaieb provided
    15 extended gcd, lcm, primes to the integers. Amine Chaieb provided
    16 another extension of the notions to the integers, and added a number
    16 another extension of the notions to the integers, and added a number