avoid duplicate import
authorhaftmann
Wed Jun 02 16:24:14 2010 +0200 (2010-06-02)
changeset 372932c9ed7478e6e
parent 37292 12a514e0319a
child 37294 a2a8216999a2
avoid duplicate import
src/HOL/Number_Theory/Cong.thy
     1.1 --- a/src/HOL/Number_Theory/Cong.thy	Wed Jun 02 16:24:14 2010 +0200
     1.2 +++ b/src/HOL/Number_Theory/Cong.thy	Wed Jun 02 16:24:14 2010 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4  header {* Congruence *}
     1.5  
     1.6  theory Cong
     1.7 -imports GCD Primes
     1.8 +imports Primes
     1.9  begin
    1.10  
    1.11  subsection {* Turn off One_nat_def *}