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
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial Remotely access PCs and mobile devices and provide instant support Improve your efficiency, and focus on delivering more value-add services Discover what IT Professionals Know. Rescue delivers http://p.sf.net/sfu/logmein_12329d2d
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
