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.
Best,
Andreas
On 15/11/15 10:38, Florian Haftmann wrote:
isabelle: f1b257607981 tip
afp: 1a688183b05a tip
Any idea what is going on here?
Florian
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
