It's also worth mentioning `~A` by PROVE_TAC[]
since it can sometimes be faster than metis_tac. On 17 November 2015 at 07:16, Ramana Kumar <[email protected]> wrote: > there are many options: > > `~A` by metis_tac[] > > `~A` by (strip_tac >> fs[]) > > first_assum(assume_tac o CONTRAPOS) >> res_tac > > first_x_assum(imp_res_tac o CONTRAPOS) > > Cases_on`A` >> fs[] > > `~A` by (spose_not_then strip_assume_tac >> res_tac) > > `~A` by (CCONTR_TAC >> fs[]) > > ... > > On 17 November 2015 at 02:25, shengyu shen <[email protected]> wrote: > >> Dear all: >> >> suppose that I have two assuptions: >> >> 1 A->B >> 2 ~B >> >> So which tactic should I use to get the conclusion ~A? >> >> Shen >> >> >> ------------------------------------------------------------------------------ >> >> _______________________________________________ >> hol-info mailing list >> [email protected] >> https://lists.sourceforge.net/lists/listinfo/hol-info >> >> >
------------------------------------------------------------------------------
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
