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



Hi  , 
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?


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