Re: [Hol-info] Improve EXISTS_TAC with by taking hints from the assumption list

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

On 28/12/2012, at 23:07, Vincent Aravantinos <vin...@gm...> 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