On 28/12/2012, at 23:07, Vincent Aravantinos <[email protected]> wrote:
> Le 27/12/12 06:55, Ramana Kumar a écrit : >> Do you have a clone of the HOL4 git repository? You could make a pull >> request on github after adding HINT_EXISTS_TAC in an appropriate place. > > I'd totally be ready to do this, but I would like, first of all, to be sure > people share my interest in the features of HINT_EXISTS_TAC: I don't want to > pollute the repo with new tactics that I am the only one to find useful. > In particular, it seems from this discussion that there are several "close" > solutions in HOL4. > However, none of them allows to just make progress in a goal without solving > it completely. > In my opinion, that's an essential aspect of HINT_EXISTS_TAC, but I'm not > sure this opinion is shared by any of you guys? :-) I think my first reaction to a clean implementation with test cases (in a selftest.sml file, say) and documentation (a .doc file) would be to accept first and ask questions later. If it turns out that something really is redundant or otherwise unloved given other facilities in the system it can always be removed. Michael ------------------------------------------------------------------------------ Master HTML5, CSS3, ASP.NET, MVC, AJAX, Knockout.js, Web API and much more. Get web development skills now with LearnDevNow - 350+ hours of step-by-step video tutorials by Microsoft MVPs and experts. SALE $99.99 this month only -- learn more at: http://p.sf.net/sfu/learnmore_122812 _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
