[isabelle] isabelle doc - where to start?




Hi,

I have to learn to use Isabelle 2017, and I can't find where to start in the documentation.

I've successfully got a theory file called HOL_Gen.thy,
and fixed all the errors which show up when I run
/home/users/jeremy/Isabelle2017/bin/isabelle process -T HOL_Gen
but now I want to develop proofs interactively.

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?

In Isabelle2005 you could get to a terminal type interface to Isar by, as I recall, using the command Isabelle instead of isabelle. Is anything like this possible in Isabelle 2017? (I've seen the reference to isabelle console, but that's for entering ML commands not Isar commands)

Thanks

Jeremy






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