I think you might have accidentally pushed to afp-2015 instead of afp-devel.
This is on afp-2015: changeset: 5536:b0b40e683dbc user: paulson <l...@cam.ac.uk> date: Thu Aug 20 17:31:45 2015 +0100 summary: fixed problems mostly connected with changes to tendsto_zero_powrI I’ll have a looks at moving the changeset over. Cheers, Gerwin > On 22.08.2015, at 21:46, Larry Paulson <l...@cam.ac.uk> wrote: > > 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. > > Larry > >> On 21 Aug 2015, at 12:31, Isabelle >> <isat...@macbroy2.informatik.tu-muenchen.de> wrote: >> >> <afp-test-devel-2015-08-21.log> > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ________________________________ The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev