You need to use completeInduct_on, as in
completeInduct_on `m + n`
Best,
Michael
On 12/12/14 09:30, Muhammad Qasim wrote:
> Hello,
>
> I am looking for an alternative of WF_INDUCT_TAC for HOL4. I would be
> greatful if someone can provide good advice. I found a link for this
> tactic but the
Hello,
I am looking for an alternative of WF_INDUCT_TAC for HOL4. I would be
greatful if someone can provide good advice. I found a link for this
tactic but the code is for hol_light.
http://mws.cs.ru.nl/~mptp/hol-flyspeck/trunk/wf.html
Looking forward to your response. Thank you.
Regards
