[isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves
andreas.lochbihler at inf.ethz.ch
Sun Nov 15 11:43:15 CET 2015
MonoBoolTranAlgebra was failing due to my change in Isabelle/90f54d9e63f2 and the removal
of theorem fun_eq in favour of arg_cong (I have not investigated when this happened, but
just adapted the proof scripts), see changesets 53f94abb8704 and 0377b757f016.
Presburger-Automata had a looping call to simp which looks related to the changes with
real. It should work now in AFP/935a90e010a2.
Vickey_Clarke_Groves looks related to the changes to "real", but I have not tried to fix this.
On 15/11/15 10:38, Florian Haftmann wrote:
> isabelle: f1b257607981 tip
> afp: 1a688183b05a tip
> Any idea what is going on here?
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev