nipkow at in.tum.de
Wed Feb 27 11:27:55 CET 2008
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!
More information about the isabelle-dev