[isabelle-dev] status (AFP)

[Gerwin Klein]

I think you might have accidentally pushed to afp-2015 instead of afp-devel.

This is on afp-2015:

changeset:   5536:b0b40e683dbc
user:        paulson <lp15 at 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 <lp15 at 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 <isatest at macbroy2.informatik.tu-muenchen.de> wrote:
>>
>> <afp-test-devel-2015-08-21.log>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at 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.