Re: [isabelle] about "imports Primes"



Unless the file you want to import is in the same folder as your theory
or it is part of the HOL session, you have to qualify it; in this case:
"HOL-Number_Theory.Primes", or even better
"HOL-Number_Theory.Number_Theory".

Cheers,

Manuel


On 2018-06-02 22:07, José Manuel Rodriguez Caballero wrote:
> 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.