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

[Florian Haftmann]

The two other failures are also reproducible interactively and seem to
result from recent changes in HOL-Probability.  Johannes, I guess this
is your part.

	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/bbf53bed/attachment.sig>