Am Mittwoch, den 06.02.2013, 12:25 +0100 schrieb Makarius: > On Tue, 5 Feb 2013, Johannes Hölzl wrote: > > > there is a bugproblem with the let-simproc, resulting in a non > > terminating simp call (Isabelle hg id = 58e2d0cd81ae, tip of > > isabelle-release): > > > > theory Scratch imports Complex_Main begin > > > > lemma "(let x = Collect P in R x x ∧ (Ball s P)) = X" > > using [[simp_trace]] > > apply simp > > > > The attached hg-bundle changes this behaviour to a terminating simproc. > > (The bundle can be applied to a repo containing #58e2d0cd81ae by > > "hg pull let_simp_betaeta.bundle") > > > > It currently runs in the testboard: > > http://isabelle.in.tum.de/testboard/Isabelle/rev/31f3b7c70a2c > > > > @Makarius: Is it possible to include this patch in Isabelle2013, when > > the testboard run is green? > > Testboard does not test very much, compared to what has been tested > manually and semi-automatically in the past 2 weeks for the release. AFP > would also have to be covered. > > Anyway, this behaviour of let_simproc seems to have been there from its > beginning, or at least back until Isabelle2011 (what is what I have > tried). Nobody has noticed a problem in several years, so this change is > for the next release, unless there are really strong reasons to revisit it > now. > > > Makarius
Thomas reported the problem to me. For me it is okay to fix it after Isabelle2013. @Thomas: Is it important for you to fix it in Isabelle2013? I hope the workaround with adding Let_def to the simplifier should work fine. Then I will add it just to the development version of Isabelle. - Johannes _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
