The tactic (tac1 THEN tac2) applies tac2 to all subgoals generated by tac1.
On 22 December 2015 at 23:05, Ada 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 w
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 sho
