# HG changeset patch # User haftmann # Date 1275488654 -7200 # Node ID 2c9ed7478e6e1b5735df10f7d1451b2679d28426 # Parent 12a514e0319a48e079a6c017f8fec7defe324be0 avoid duplicate import diff -r 12a514e0319a -r 2c9ed7478e6e src/HOL/Number_Theory/Cong.thy --- a/src/HOL/Number_Theory/Cong.thy Wed Jun 02 16:24:14 2010 +0200 +++ b/src/HOL/Number_Theory/Cong.thy Wed Jun 02 16:24:14 2010 +0200 @@ -30,7 +30,7 @@ header {* Congruence *} theory Cong -imports GCD Primes +imports Primes begin subsection {* Turn off One_nat_def *}