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.

Isabelle/jEdit is primarily an editor. As such, you may of course edit
unsaved files, but there is no good reason to. When you start your
theory, you can directly save it without waiting until your program
exits. Press "Ctrl-S" (or "Cmd-S" on a Mac I believe) to save and select
a more appropriate location.

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

Path-qualified names have to be enclosed in double quotes.

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

Isabelle will always, with some exceptions like "Main", look for imports
relative to the location of the theory you are editing. There is, as far
as I know, no way to change this (and it is hardly necessary).

(However, it is also possible to use so-called session-qualified
imports. Whether or not that is necessary depends on your project.)

There is a dedicated manual for Isabelle/jEdit:
<https://isabelle.in.tum.de/dist/Isabelle2017/doc/jedit.pdf>

Hope that helps!




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