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




Hi Lars,

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

I tried the suggestion of a path name, but it didn't seem to like the symbol /

How do I tell this tool where to look for theory files? And is its use documented anywhere?

Cheers,

Jeremy

On 24/05/18 16:32, Lars Hupel wrote:
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.