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

theory Scratch
  imports HOL_Gen


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


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