[isabelle-dev] HOL-IMP very slow

[Jasmin Blanchette]

Am 12.02.2014 um 19:40 schrieb Makarius <makarius at sketis.net>:

> In principle the concept of "bound" variable in the context can do that, see also Variable.next_bound.  It enumerates local variables in a way such that the usual term order (the one of the Simplifier) coincides with the enumeration order.

Good to know. I might end up using it.

>> 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.

Jasmin