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