[isabelle-dev] Problem

Tobias Nipkow 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 mailing list