*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: [isabelle] about "imports Primes"*From*: José Manuel Rodriguez Caballero <josephcmac at gmail.com>*Date*: Sat, 2 Jun 2018 22:07:08 +0200

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.

**Follow-Ups**:**Re: [isabelle] about "imports Primes"***From:*Manuel Eberl

- Previous by Date: [isabelle] Type Theory vs. Set Theory (HOL, Isabelle/HOL, Q0, and R0 vs. ZFC) – Re: [Metamath] [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)
- Next by Date: Re: [isabelle] about "imports Primes"
- Previous by Thread: [isabelle] Type Theory vs. Set Theory (HOL, Isabelle/HOL, Q0, and R0 vs. ZFC) – Re: [Metamath] [Coq-Club] A criticism to CIC from the point of view of foundations of mathematics (Voevodsky's argument)
- Next by Thread: Re: [isabelle] about "imports Primes"
- Cl-isabelle-users June 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list