Surely the main issue that blast somehow behaves differently depending upon which machine it’s running on?
Larry > On 31 Aug 2018, at 22:35, Makarius <makar...@sketis.net> wrote: > > 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
