src/HOL/Number_Theory/Cong.thy
changeset 33718 06e9aff51d17
parent 32479 521cc9bf2958
child 35644 d20cf282342e
equal deleted inserted replaced
33717:c03edebe7408 33718:06e9aff51d17
    18 another extension of the notions to the integers, and added a number
    18 another extension of the notions to the integers, and added a number
    19 of results to "Primes" and "GCD". 
    19 of results to "Primes" and "GCD". 
    20 
    20 
    21 The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
    21 The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
    22 developed the congruence relations on the integers. The notion was
    22 developed the congruence relations on the integers. The notion was
    23 extended to the natural numbers by Chiaeb. Jeremy Avigad combined
    23 extended to the natural numbers by Chaieb. Jeremy Avigad combined
    24 these, revised and tidied them, made the development uniform for the
    24 these, revised and tidied them, made the development uniform for the
    25 natural numbers and the integers, and added a number of new theorems.
    25 natural numbers and the integers, and added a number of new theorems.
    26 
    26 
    27 *)
    27 *)
    28 
    28