The tactic (tac1 THEN tac2) applies tac2 to all subgoals generated by tac1.
On 22 December 2015 at 23:05, Ada <[email protected]> wrote: > Hey guys, > > I am learning to use HOL4. In listTheory , I found that: > val DROP_0 = store_thm( > "DROP_0", > ``DROP 0 l = l``, > Induct_on `l` THEN SRW_TAC [] []); > I was wondering that after "Induct_on `l`", there should be two subgoals. > But the following was "THEN SRW_TAC [] []", I thought it should be the form > of > THENL [ _ , _ ]. Why could "THEN SRW_TAC [] []" succeed? And what are the > conditions to use it? > > Thanks! --Wish. > > > ------------------------------------------------------------------------------ > > _______________________________________________ > 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
