On Tue, 28 May 2013, Stefan Berghofer wrote:
Types as well as terms are unified. The outermost functions assume
the terms to be unified already have the same type. In resolution,
this is assured because both have type "prop".
One more aspect here: HO unification is also used on flex-flex pairs,
which might have different types. The unify implementation might
correctly produce equal types for other reasons nonetheless, but the
"proof" above would have to be adapted.
Note that the marginal change 6228806b2605 in metis_reconstruct.ML is
related to that: without applying the type instantiation on the matched
flex-flex pairs it could break down.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
