[isabelle-dev] isabelle test failures

Lukas Bulwahn bulwahn at in.tum.de
Wed Jan 11 09:16:49 CET 2012

Hi all,

the latest failures of the isabelle test of the form:

     Conflicting definitions for `ad'
     Bound at: /tmp/isabelle-isatest25132/Quickcheck_Narrowing6407933/Generated_Code.hs:XXXX:XX-XX
     In a case alternative

causing quickcheck to fail in ex/Tree23.thy is not related to any modifications in quickcheck, but is probably related to some recent changes in the code generator or some setup on macbroy21.


More information about the isabelle-dev mailing list