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

[Florian Haftmann]

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

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140618/e0aa451f/attachment.sig>