Re: [isabelle] modus tollens rule in isabelle



On Fr, 2015-02-27 at 19:13 +0100, mahmoud abdelazim wrote:
> Does exists a modus tollens rule in isabelle?
> 

You may try

  HOL.contrapos_nn: â ?Q; ?P â ?Qâ â  ?P

or just prove the rule you need "by blast"

--
  Peter





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