Re: [isabelle] Problems with Sequents in Isabelle



On Thu, 8 Feb 2007, Peter Chapman wrote:

> I am getting problems when trying to use the Sequents logic for 
> Isabelle.  I'm using XEmacs from the Fink package downloader and 
> Isabelle2005, on a PowerPC mac.  I've compiled the logic Sequents, and 
> once in Proof General switched to using this from the Isabelle --> 
> Logics --> Sequents menu option.

> context LK.thy
> 
> 	***Outer syntax error : name declaration expected but long identifier
> "LK.thy" was found
> 

> Goal "|- A /\ B --> A";
> 
> I get the error
> 
> ***  Outer syntax error: command expected, but identifier "Goal" was found
> 
>
> Basically, I'm not sure what has gone wrong; I don't think Isabelle is 
> working properly at all.

The above commands refer to the old ML toplevel of Isabelle, but the 
ProofGeneral setup uses the Isar toplevel, which is described in the 
isar-ref manual.

In order to see how this works for Sequents, just open one of the example 
theories, e.g. Sequents/LK/Nat.thy and start stepping through the source. 
In Isabelle2005 these theories still have an appendix in ML with the 
actual proofs, but it is hard to use these with ProofGeneral.  In recent 
development snapshots of Isabelle (cf. http://isabelle.in.tum.de/devel/) 
everything has been converted into proper theory sources already.


	Makarius






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