[isabelle-dev] Build problems in AFP with current tips
florian.haftmann at informatik.tu-muenchen.de
Wed Jun 18 22:15:16 CEST 2014
thanks for spending time on this.
Concerning Completeness, I had a second look and found out:
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!?
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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 263 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev