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

[Makarius]

On Mon, 17 Mar 2008, Makarius wrote:

> On Mon, 17 Mar 2008, Tobias Nipkow wrote:
> 
> > When I run AFP/Group-Ring-Module, it fails:
> > 
> > *** empty result sequence -- proof command failed
> > *** At command "apply" (line 6032 of 
> > "/mnt/home/nipkow/AFP/afp-devel/thys/Group-Ring-Module/Algebra1.thy").
> 
> I have almost isolated that problem.  Stay tuned.

We should be back to normal now.  Actually this problem was my fault, the 
result of trying to write papers and ``optimize'' the system (notably 
locales) at the same time.


	Makarius