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