[isabelle-dev] Isabelle repository broken

Jasmin Blanchette jasmin.blanchette at inria.fr
Tue May 24 17:22:48 CEST 2016


On 24.05.2016, at 17:12, Makarius <makarius at sketis.net> wrote:
> 
> The Isabelle repository is broken at 76cb6c6bd7b8 (paulson) or
> 6a17bcddd6c2 (eberlm).
> 
> The failure is as follows:
> ### theory "Generate_Binary_Nat"
> ### 197.201s elapsed time, 259.420s cpu time, 8.924s GC time
> *** "List.coset" is not a constructor, on left hand side of equation, in
> theorem:
> *** permutations_of_set (List.coset ?xs) \<equiv>
> ...

Looking at the history, it's hard to believe the culprit would be anything but change dd651e3f7413.

Jasmin




More information about the isabelle-dev mailing list