On 01/09/18 14:39, Manuel Eberl wrote: >> This thread consists of two sub-threads. The hardware / OS question >> still needs to be sorted out: it might be something with Arch Linux. > > I don't really have much of an opportunity to test this on other systems > atm, but I'll see what I can do. > >> 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? > > Even if it is, it has no preconditions, so I don't see how it could > cause nontermination.
This is where Larry could take a closer look. The argument ?f of function type (with sort constraints) looks like a candidate for unexpected problems. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev