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

[Vincent A. <vin...@gm...>]

Le 28/12/12 08:01, Thomas Tuerk a écrit :
> Dear Vincent,
>
>> I see. I'll have a look for my culture, but I think in the end that it
>> will be simpler, if I need it, to just translate my current HINT_EXISTS_TAC to
>> HOL4 (roughly nothing more than Ocaml->SML). I'll have a look at
>> quantHeuristicsLib when I get the time though, because maybe the
>> my problem will actually happen to be useless in the end.
> this makes sense. Using quantHeuristicsLib or consequence conversions would provide
> you with a bit more power. However, to solve exactly the problem you described,
> it is really easier to just port your OCaml code.
>
> I might be interested in your problem in general, though. I still look for
> users for my quantifier heuristic library. I implemented this library as
> an extensible one than can easily be extended by the user.
> What kind of quantifier problems do you have?
> Is there some other kind of automation you might be interested in.
I don't know yet. It will depend on my practical needs. I'll tell you if 
I find something that can be of interest.


Cheers,
V.