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"


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