Re: [isabelle] Fwd: [Isabelle] Failed to parse prop



Hi  Lars,
After  tried,  it  return  inner syntax  error, where is wrong?
theory Scratchimports Mainbegin(*lemma "A ∨ (B ∨ A) ⇒ B ∨ (A ∨ B)"*)lemma "A ∨ (B ∨ A) → B ∨ (A ∨ B)"by blastend

Regards,
Martin  Lee
> Date: Thu, 9 Apr 2015 11:20:42 +0200
> From: noschinl at in.tum.de
> To: cl-isabelle-users at lists.cam.ac.uk
> Subject: Re: [isabelle] Fwd: [Isabelle] Failed to parse prop
> 
> On 08.04.2015 22:58, Martin Lee wrote:
> > Hi sir,
> >
> > theory Scratch
> > imports Pure
> You need to import Main. Importing Pure is almost always the wrong thing
> to do.
> 
 		 	   		  


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