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

[Lawrence Paulson]

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")