Fixed in AFP 833ddc4860dd. - Johannes
Am Mittwoch, den 18.06.2014, 22:32 +0200 schrieb Florian Haftmann: > The two other failures are also reproducible interactively and seem to > result from recent changes in HOL-Probability. Johannes, I guess this > is your part. > > Florian > > On 18.06.2014 21:39, Lawrence Paulson wrote: > > Strange — I took a look (with the latest versions, same ids as quoted) and > > it was fine. > > > > > > On 18 Jun 2014, at 18:47, Florian Haftmann > > <florian.haftm...@informatik.tu-muenchen.de> wrote: > > > >> isabelle: 88263522c31e tip > >> afp: b514f0bac50e tip > >> > >> Completeness FAILED > >> *** Failed to load theory "Soundness" (unresolved "Completeness") > >> *** Extra variables on rhs: "founded", "bounded" > >> *** The error(s) above occurred in definition: > >> *** "proofTree A == bounded A & founded subs (SATAxiom o sequent) A" > >> *** At command "definition" (line 70 of > >> "/mnt/home/haftmann/data/afp/master/thys/Completeness/Completeness.thy") > > > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
