[isabelle-dev] status (AFP)

Larry Paulson lp15 at cam.ac.uk
Sat Aug 22 13:46:07 CEST 2015

The error is as follows:

> *** Undefined fact: "setsum_bounded" (line 286 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/Girth_Chromatic/Ugraphs.thy")
> *** At command "using" (line 286 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/Girth_Chromatic/Ugraphs.thy”)

Yes, I renamed this theorem to setsum_bounded_above, but I fixed it in afp/devel in the afternoon of 20 August. And committed and pushed my changes. Why this error still occurs, I have no idea.


> On 21 Aug 2015, at 12:31, Isabelle <isatest at macbroy2.informatik.tu-muenchen.de> wrote:
> <afp-test-devel-2015-08-21.log>

More information about the isabelle-dev mailing list