Re: [isabelle] Trouble loading theories on windows (Isabelle2013-1-RC3)
There's no problem. I misspelled "FSet" as "Fset".
Actually, I guess there is a problem that leads to confusion.
Because Windows filenames aren't case sensitive, the "imports" command
will load the file "FSet.thy" when importing "~~/src/HOL/Library/Fset",
though jEdit loads it with the wrong case, "Fset.thy", and the error stays.
The import of
will load the file with the right case into jEdit, "FSet.thy", and it
I discovered all that after importing
"~~/src/HOL/Library/Code_Target_Nat" to get the pretty printing of
natural numbers, mentioned by Andreas in this email:
That's very useful.
On 10/30/2013 6:02 PM, Gottfried Barrow wrote:
This is a continuation of this thread: "[isabelle] Trouble loading
theories on windows":
It's not specific to Isabelle2013-1, but I go ahead and associate it
The suggestions are to save and reload the theory, but that doesn't
work for me when I use this:
imports Complex_Main "~~/src/HOL/Library/Fset"
The file Fset.thy gets loaded into jEdit, but I still get this error:
Bad theory (file
So, I use a relative path:
The file Fset.thy gets loaded, I get no errors, and I don't have to do
This archive was generated by a fusion of
Pipermail (Mailman edition) and