[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP
makarius at sketis.net
Fri Aug 31 23:35:09 CEST 2018
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.
More information about the isabelle-dev