[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