Re: [isabelle] isabelle doc - where to start?



Dear Jeremy,

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
following:


theory Scratch
  imports HOL_Gen

begin

lemma ...

but it complains
Bad theory import "Draft.HOL_Gen"

What would be going wrong here? Is the use of this tool documented anywhere?

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).

Cheers
Lars




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