Re: [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: isat...@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.

smime.p7s
Description: S/MIME Cryptographic Signature

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev