> 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. Manuel _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev