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



Iâm afraid your input syntax is incorrect. See the documentation for details, e.g. 

http://isabelle.in.tum.de/dist/Isabelle2014/doc/prog-prove.pdf

And there are plenty of examples in src/HOL/ex/Classical.thy.

Larry Paulson


> On 8 Apr 2015, at 21:58, Martin Lee <martinchan2016 at gmail.com> wrote:
> 
> Hi sir,
> 
> theory Scratch
> imports Pure
> begin
> lemma shows "[P â Q; P â Q] â Q â P"
> apply (auto)
> done
> lemma shows "A â (B â A) â B â (A â B"
> apply (auto)
> done
> end
> 
> -- 
> Regards,
> Martin





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