[isabelle-dev] HOL-IMP very slow
jasmin.blanchette at gmail.com
Wed Feb 12 20:28:56 CET 2014
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.
More information about the isabelle-dev