Re: [isabelle] Fwd: [Isabelle] Failed to parse prop
i succeed to run after following example,
but the subgoal is the same as the original lemma,
i guess that it proved directly with logic table.
one number can have many kinds of representation of logic
0010 , And(A,Or(B,.... Or(And(A,B..... etc
A -> B , between A and B, there can be many ways. is this the reason that only one subgoal when prove this?
is resolution algorithm for generating subgoals? if not, what algorithm do it used to generate subgoal?
> From: tesleft at hotmail.com
> To: noschinl at in.tum.de; cl-isabelle-users at lists.cam.ac.uk
> Date: Fri, 10 Apr 2015 04:44:12 +0800
> Subject: 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
> 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