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