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



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 		 	   		  


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