[isabelle-dev] Build problems in AFP with current tips

[Johannes Hölzl]

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.haftmann at 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")
> > 
>