[isabelle-dev] HOL-IMP very slow

[Jasmin Blanchette]

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

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

I can't help much there. Perhaps Larry knows more. All I can recall is that Metis sometimes suggests type instantiations (since types are encoded as terms, and type variables as term variables), but that in "metis" these are ignored for some reason, sometimes leading to more polymorphic theorems on the Isabelle side of things than on the Metis side.

Jasmin