[isabelle-dev] Problem

[Tobias Nipkow]

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