[isabelle-dev] Bad state of repository

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Tue Jul 1 23:11:46 CEST 2014

Am 01.07.2014 um 22:33 schrieb Makarius <makarius at 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.


More information about the isabelle-dev mailing list