chaieb at in.tum.de
Wed Feb 27 11:44:23 CET 2008
Sorry all, This someone was me --- I added a rule Suc 0 ^ n = Suc 0 and
the proofs went wrong -- I'll fix it.
Tobias Nipkow wrote:
> Yesterday and today 3 AFP theories failed: Fermat3_4, RSAPSS,
> SumSquares. Amine traced it to the following problem:
> Somebody has modified simp or auto (most likely by removing a simp rule)
> and now "EX k. a = k^n" is no longer proved from a*b =1 und b = 1.
> The problem was probably introduced 2 days ago.
> Please, do test your modifications against the AFP as well!
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev