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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
