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
