Am 12.02.2014 um 20:40 schrieb Makarius <[email protected]>: > 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
