On 31/08/18 22:00, Manuel Eberl wrote:
> That's interesting. I suspected one of the "continuous_on" rules would
> be the cause. In any case, I don't know how the unification works
> exactly w.r.t. sorts, but the "continuous_on_discrete" rule does not
> apply to this goal at all due to its restrictive type class constraint.
Blast does its own unification, without taking fully account of types
and type classes. The found proof is then reconstructed as in "fast" and
its friends, using regular Isabelle term + type unification.
Larry should be able to say more precisely, what the limits of blast are.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
