Re: [isabelle] Trouble loading theories on windows



I have also received a similar error on Linux in the recent past whilst
trying to load the Nominal.thy from Nominal Isabelle.  Similarly, the
problem disappears when the theory file is saved, suddenly loading
correctly.

Thanks,
Dom

On Wed, 2013-08-21 at 16:09 +0900, Christian Sternagel wrote:
> Dear Jason,
> 
> if I do what you describe (on linux though) I get the same error until I 
> *save* the new theory file (which causes jEdit to actually process the 
> imports). (The same thing does not occur when just importing "Main", I 
> guess the difference is that "Main" is part of the default logic image 
> "HOL", but "Primes" isn't.)
> 
> hope this helps,
> 
> chris
> 
> On 08/21/2013 03:00 PM, Jason Dagit wrote:
> > Hello,
> >
> > I installed Isabelle 2013 for windows (windows 7). If I put this into jEdit:
> > ```
> > theory Scratch
> > imports Complex_Main "~~/src/HOL/Number_Theory/Primes"
> > begin
> > ```
> > It gives me this error: Bad theory (file
> > "C:\Users\dagit\Desktop\Isabelle2013\src\HOL\Number_Theory\Primes.thy")
> >
> > If I copy the path from that error message and try to use it with some
> > other program it works just fine.
> >
> > I've also tried this with the isabelle eclipse IDE. I get the same error
> > but a slightly different formatting for the path.
> >
> > Any ideas how to fix this?
> >
> > Thanks,
> > Jason
> >
> 
> 






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