Re: [isabelle] Trouble loading theories on windows



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.