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
