Re: [Hol-info] Learning HOL Light

[Michael N. <Mic...@ni...>]

On 18/12/12 6:04 PM, Bill Richter wrote:
> But I really don't understand why Michael's STRIP_TAC works.  P 48 of the tutorial says 
> STRIP_TAC has the effect of DISCH_TAC, GEN_TAC or CONJ_TAC.
> At the time we use it, we have only the goal

> `(?s. s 0 = p /\ s 4 = p' /\ (!m. m < 4 ==> s (SUC m) = SUC (s m)))
>  ==> (?q. (?s. s 0 = p /\ s 3 = q /\ (!m. m < 3 ==> s (SUC m) = SUC (s m))) /\
>           p' = SUC q)`

> So I thought that STRIP_TAC here meant DISCH_TAC, which of course has the effect:

I guess you've found a bug in the documentation.  The implementation of
STRIP_TAC will actually be calling

   DISCH_THEN STRIP_ASSUME_TAC

in the situation above, not

   DISCH_TAC

which, by way of contrast, is more or less equivalent to

   DISCH_THEN ASSUME_TAC

Michael