Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] about "imports Primes"

Email Gateway (Aug 22 2022 at 17:32):

From: Manuel Eberl <eberlm@in.tum.de>
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

Last updated: Apr 23 2024 at 20:15 UTC