[isabelle-dev] AFP/Group-Ring-Module

Tobias Nipkow nipkow at in.tum.de
Mon Mar 17 08:04:17 CET 2008

When I run AFP/Group-Ring-Module, it fails:

*** empty result sequence -- proof command failed
*** At command "apply" (line 6032 of 

I don't think this is caused by my own change but must have been there 
for a couple of days. (It seems like the daily AFP test is not working 
at the moment.)

I looked at the problem and it appears that the ALL/--> structure of a 
formula after simplification with *locale* stuff has changed....


More information about the isabelle-dev mailing list