[isabelle-dev] Problem

[Amine Chaieb]

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