Re: [isabelle] Setting up a logic: need instructions.

Hi Bart,

I would be interested why you feel it necessary to set up a new logic.
To get anywhere requires an enormous amount of ground work. I can
understand that as a mathematician you may not like HOL, but ZF might be
more to your taste - and although not as well developed as HOL, it is
still a lot better than nothing.


Bart Kastermans wrote:
> I am trying to better understand how logics that come with Isabelle are
> set up, and how to set up my own.  Is there any good documentation on
> this?  Explaining the use of TrueProp, and say all the commands in the
> first 150 lines of a file like IFOL.thy .
> Thanks.
> Best,
> bart

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