[isabelle-dev] Fwd: test failed (Archive of Formal Proofs)

[Tobias Nipkow]

I hope I fixed that this morning.

Tobias

On 18/06/2015 21:31, Larry Paulson wrote:
> Looks like a recent change has broken Nominal2:
>
> *** Failed to load theory "Nominal2_Abs" (unresolved "Nominal2_Base")
> *** Failed to load theory "Nominal2_FCB" (unresolved "Nominal2_Abs")
> *** Failed to load theory "Nominal2" (unresolved "Nominal2_Abs", "Nominal2_Base", "Nominal2_FCB")
> *** Theorem must be of the form "?p \<bullet> c \<equiv> c", with c a constant or fixed parameter:
> *** ?p \<bullet> ?y == ?y
> *** At command "lemma" (line 2123 of "/mnt/nfsbroy/home/isatest/afp/devel/thys/Nominal2/Nominal2_Base.thy")
>
> Larry
>
>> Begin forwarded message:
>>
>> From: isatest at macbroy2.informatik.tu-muenchen.de (Isabelle )
>> Subject: test failed (Archive of Formal Proofs)
>> Date: 18 June 2015 11:25:01 BST
>> To: undisclosed-recipients:;
>>
>> Session [Incompleteness] in the automated afp test failed.
>>
>> AFP version: development -- hg id dd9b5f6f3866
>> Isabelle version: devel -- hg id e0169291b31c
>> Test ended on: macbroy2, Thu Jun 18 12:25:01 CEST 2015.
>>
>> To reproduce the error, check out the development version of the
>> archive from sourceforge and run "isabelle make" on your session.
>>
>> This is an automatically generated email. To switch off these
>> notifications, edit thys/Incompleteness/config and hg commit and push the changes.
>>
>> Have a nice day,
>>   isatest
>>
>>
>> This body part will be downloaded on demand.
>>
>>
>> This body part will be downloaded on demand.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5112 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150619/b31d1a35/attachment.bin>