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
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
