makarius at sketis.net
Mon Mar 17 21:13:43 CET 2008
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.
More information about the isabelle-dev