I'm sorry, it's the HOL Light tactic DISCH_TAC, not MATCH_MP_TAC, that's much the same as the way the miz3 thesis changes from α ⇒ β to β after writing assume α; And DISCH_TAC is part of STRIP_TAC, which also includes GEN_TAC, which is much the same as the way the miz3 thesis changes from ∀ x:A. α to α after writing let x be A; I don't see how to relate MATCH_MP_TAC to miz3 thesis changes. Given a theorem XXX that implies α ⇒ β, and our goal is something β, then MATCH_MP_TAC[XXX] changes our goal to α. In a miz3 proof, if β is is the thesis, one proves α, and then writes qed by XXX; So I don't have the by justification figured out. I'm off to the blackboard!
-- Best, Bill ------------------------------------------------------------------------------ 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
