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

[Larry Paulson]

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
> 
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: afp-test-devel-2015-06-18.log
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20150618/2a6dbf9f/attachment-0001.log>
-------------- next part --------------
>