[isabelle-dev] AFP

[Makarius]

On Thu, 15 May 2014, Jasmin Christian Blanchette wrote:

> 2nd wave: Nominal2, Incompleteness, Launchbury. Here I didn't 
> investigate much, but from the Nominal2 failure I get the impression 
> that some Pure ML signature has been changed.

That's me.  It is a trivial breakdown due to one of my recent Pure 
cleanups.  I have updated that in AFP/ed0dfdd2b00d.

We also have a total failure of existence with isatest, since HOL-Proofs 
does not build on the initial test machine (lxbroy2) for the documentation 
sessions.  I still need to find out if it is the one lemma addition by 
Tobias, my change of Poly/ML, or just that machine which is constantly 
running some boring batch process: on all cores: 178027:57 diam_5


 	Makarius