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

Hi Sebastian,

Thanks - so far as I can see this gives me (almost) the same result as I had by running the executable called Isabelle2017, with the same issues


On 24/05/18 16:20, Sebastien Gouezel wrote:
Le 24/05/2018 à 04:59, Jeremy Dawson a écrit :


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.

/home/users/jeremy/Isabelle2017/bin/isabelle jedit
to open the interactive editor.


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