Re: [isabelle] what is the correct syntax to do simple auto prove proposition

Hi Martin,

Am 26.05.2014 um 05:22 schrieb Lee Martin CCNP <tesleft at>:

> Hi sir,
> After choose sledgerhammer, and check isar proof and click Apply, got error
> what is the correct syntax to prove simple proposition
> Illegal application of command "lemma" at top level
> lemma "(a ∨ b) ∧ (b ∨ c) --> (a ∨ c)"apply autodone

Is this your entire theory file? If so, you will need to start with the usual header. Assuming your theory file is called Foo.thy, this means:

    theory Foo
    imports Main

This should be explained in the tutorials (the first two bullet points at



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