[isabelle] isabelle doc - where to start?
I have to learn to use Isabelle 2017, and I can't find where to start in
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:
but it complains
Bad theory import "Draft.HOL_Gen"
What would be going wrong here? Is the use of this tool documented
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)
This archive was generated by a fusion of
Pipermail (Mailman edition) and