[isabelle] about "imports Primes"



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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.