# [isabelle] Problems with Sequents in Isabelle

Hi

`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.
`

`Following the manual (.../doc/Logics.pdf) I type in "context LK.thy"
``But then I get the following error messages
`
context LK.thy

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

` *** Could not find theory file "LK.thy.thy" in dir(s) "/Users/pc/
``Isabelle/Proof Files", "."
`` *** Theory loader: the error(s) above occurred while
``examining theory "LK.thy"
` *** At command "context"
but from typing
context "LK"
I get the message
theory LK = (LK)

`Now, again following the example in the Logics manual, if I type the
``following
`
consts A, B :: o;
I get an error of
*** Outer Syntax error: keyword "::" expected but keyword "," was found
Changing this to
consts A :: o
B :: o;

`Allows it to work. However, now if I try to prove the simple sequent
``" |- A /\ B --> A" via the line
`
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. I also experienced a problem when trying
``to prove automatically that the sum of the first n squares is (1/6)n(n
``+1)(2n+1), in that Isabelle cannot do it by "auto" or any other
``method (this was back in HOL). The proof of the sum of the first n
``integers being (1/2)n(n+1) works fine by induction, and since by hand
``the proofs follow the same pattern and are very similar, I assume
``that the first n squares proof would be similarly easy. When I
``turned on the simplifier trace for this problem to see what was
``happening, it did not stop, and one time actually shut down XEmacs
``and left me looking at a blank X-Term window.
`
Any insights anyone could give me would be greatly appreciated.
Many thanks
Peter Chapman

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