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

On Wed, 24 Feb 2010, 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?

Section 2.3 of the isar-ref manual demonstrates the "purity" of the Isar language by definining first-order logic and doing some basic reasoning.

This is a nice example for everything, except the hairy tool setup.


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