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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and