[isabelle-dev] AFP failures in sessions ConcurrentGC, MonoBoolTranAlgebra, Presburger-Automata, Vickrey_Clarke_Groves

[Andreas Lochbihler]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>