Thanks, Petros! It will take me a while to digest your post. BTW I was wrong about the HOL Light reference manual treatment of STRIP_TAC, which is fine.
> BTW how does HOL and Informatics fit together? How do they not? :) They are connected in so many ways... I think hol-info ought to have much more info about how HOL is used in the real world. Why not more details! (Note how DISCH_TAC is *roughly* equivalent to DISCH_THEN ASSUME_TAC.) Michael posted that too, and I'm confused. I think DISCH_TAC is exactly DISCH_THEN ASSUME_TAC. A thm_tactic roughly corresponds to a forward reasoning step, whereas a tactic roughly corresponds to a backwards step. I'm missing the boat about forward & backwards. I don't know how to prove anything except as one does in miz3, and as John (and maybe I) showed, it only takes a few lines of code to write up the miz3 reasoning cleanly in HOL tactics. A thm_tactic expects a theorem (often one of the assumptions) as an argument, and does something with it (its conclusion to be more precise). I would say that's true for ASSUME_TAC, MP_TAC and DISCH_TAC, but they're described differently in manual: FIRST_ASSUM : thm_tactic -> tactic DISCH_THEN : thm_tactic -> tactic SUBGOAL_THEN : term -> thm_tactic -> tactic ASSUME_TAC : thm_tactic MP_TAC : thm_tactic DISCH_TAC : tactic Seems to me that thm_tactic means something that can't begin a command, but can be the argument of something like FIRST_ASSUM, DISCH_THEN or SUBGOAL_THEN `t`, while a tactic can begin a command. I'll go read your post more carefully! -- Best, Bill ------------------------------------------------------------------------------ Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS, MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft MVPs and experts. ON SALE this month only -- learn more at: http://p.sf.net/sfu/learnmore_122712 _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
