Hello, In "HOL/Number_Theory/Cong.thy" it is written "imports Primes", but my jEdit shows the message "Bad theory import "Draft.Primes". The same problem happens with "imports UniqueFactorization". How could I use the lemmas from these libraries, e.g., chinese_remainder? By the way, "imports GCD" works very well. Kind Regards, José M.