Am 01.07.2014 um 22:33 schrieb Makarius <makar...@sketis.net>: > One round of manual bisection yields the following, within the usual margin > of error: > > changeset: 57470:9512b867259c > user: blanchet > date: Tue Jul 01 16:49:25 2014 +0200 > summary: fixed soundness bug in monotonicity-based type encodings -- the > helper facts must be considered too
Indeed, this "obviously safe" change to Sledgehammer could as an unexpected side effect send "metis" spinning. I'm taking it back from now. Sorry for the trouble. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
