This thread consists of two sub-threads. The hardware / OS question
still needs to be sorted out: it might be something with Arch Linux.
Apart from that, my reading of blast.ML is that the "continuous_on" rule
is applied in the search independently of its fine-grained type
information. Is that correct?
Makarius
On 01/09/18 13:19, Lawrence Paulson wrote:
> 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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
