[isabelle-dev] AFP

[Tobias Nipkow]

I refrained from adding the problematic metis proofs and merely added a simp
proof. But who knows.

Tobias

On 15/05/2014 21:03, Makarius wrote:
> 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