[isabelle-dev] Bad state of repository

[Jasmin Christian Blanchette]

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.

Jasmin