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

Jeremy

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

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.

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

Sebastien






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