Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] about "imports Primes"

view this post on Zulip Email Gateway (Aug 22 2022 at 17:31):

From: José Manuel Rodriguez Caballero <josephcmac@gmail.com>
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.

Last updated: Apr 23 2024 at 08:19 UTC