[isabelle-dev] HOL-IMP very slow

[Makarius]

On Wed, 12 Feb 2014, Jasmin Blanchette wrote:

>>> Metis is a FO ATP developed by Hurd. "metis" is a higher-order proof 
>>> method (and tactic) that translates HOL to FOL (like Sledgehammer 
>>> does), developed by Paulson & Susanto.
>>
>> Do you understand yourself how that works?
>
> Does "that" refer to Metis or "metis"? I've never looked much under 
> Metis's hood except to tweak its options. For "metis", the answer is a 
> qualified yes.

Mainly the proof reconstruction on the Isabelle side, especially the 
question of type variables.

See also 568b2cd65d50: the long comment in the source after the change 
looks like the recently introduced reform of Thm.bicompose (0fa3b456a267) 
might help here, but it didn't.  Or maybe I was just confused about 8 
different modes of that function.  (One of the booleans is only required 
for this particular instance, IIRC.)


 	Makarius