Hi Larry, thanks for spending time on this.
Concerning Completeness, I had a second look and found out: http://isabelle.in.tum.de/repos/isabelle/rev/cddaf5b93728 introduces Tree.thy into HOL-Library. Hence, sessions building upon HOL-Library image cannot introduce any Tree.thy themselves. Maybe it is best to base Completeness on HOL instead!? 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") > -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
