Sorry all, This someone was me --- I added a rule Suc 0 ^ n = Suc 0 and the proofs went wrong -- I'll fix it.
Amine. 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! > > Tobias > _______________________________________________ > Isabelle-dev mailing list > Isabelle-dev at mailbroy.informatik.tu-muenchen.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
