Re: [isabelle] isabelle doc - where to start?
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and