Am 03.09.2010 um 13:37 schrieb Makarius: > Today's isatest indicates a significant drop in performance: > > http://isabelle.in.tum.de/devel/stats/at-poly/HOL-Metis_Examples.png > http://isabelle.in.tum.de/devel/stats/mac-poly-M4/HOL-Metis_Examples.png > http://isabelle.in.tum.de/devel/stats/mac-poly-M8/HOL-Metis_Examples.png
I added definitional CNF to Metis yesterday, which had a positive effect on HOL and a neutral effect on the 1600 or so successful goals from the Judgement Day suite. I'll revert this and reintroduce it if and when it can be done without harming Metis_Examples (and other apps). (In fact, Larry now suggested I avoid clausification altogether, which I will investigate in the coming months.) Thanks for spotting this and letting us know! Jasmin _______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
