Re: [isabelle] isabelle doc - where to start?
Thanks - there is no file Scratch.thy until the program offers to create
one, when I try to close it (ie, this Isabelle/jEdit window), but then
it offers to create it in my home directory.
So if I copy the file HOL_Gen.thy to my home directory, then I make more
progress. But I don't want my home directory cluttered up with Isabelle
I tried the suggestion of a path name, but it didn't seem to like the
How do I tell this tool where to look for theory files? And is its use
On 24/05/18 16:32, Lars Hupel wrote:
When I run the executable called Isabelle2017, I get a window with
multiple subwindows, but I gather from seeing this sort of thing in
the past that maybe I should type in there something like the
but it complains
Bad theory import "Draft.HOL_Gen"
What would be going wrong here? Is the use of this tool documented
this looks like it is an Isabelle/jEdit window.
Importing without any qualifiers (in your example, "HOL_Gen"), should
work fine, given that the referenced theory file resides in the same
directory as your "Scratch.thy". It looks like this is not the case. You
can save the file there, or alternatively, use a path name as import,
i.e. "path/to/HOL_Gen" (absolute paths are discouraged these days, though).
This archive was generated by a fusion of
Pipermail (Mailman edition) and