*To*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] what is the correct syntax to do simple auto prove proposition*From*: Lee Martin CCNP <tesleft at hotmail.com>*Date*: Mon, 26 May 2014 11:22:18 +0800*Importance*: Normal

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 Regards, Martin

**Follow-Ups**:**Re: [isabelle] what is the correct syntax to do simple auto prove proposition***From:*Jasmin Blanchette

- Previous by Date: [isabelle] 2 new AFP entries
- Next by Date: Re: [isabelle] what is the correct syntax to do simple auto prove proposition
- Previous by Thread: [isabelle] 2 new AFP entries
- Next by Thread: Re: [isabelle] what is the correct syntax to do simple auto prove proposition
- Cl-isabelle-users May 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list