src/HOL/Number_Theory/Cong.thy
changeset 37293 2c9ed7478e6e
parent 36350 bc7982c54e37
child 41541 1fa4725c4656
     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 *}