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
