Re: [isabelle-dev] Problem with let-simproc

2013-02-06 Thread Thomas Sewell
I'd forgotten I'd ever reported this to you. My problems with let_simproc run a little deeper anyway, and I've moved to a different approach in the meanwhile. Sorry if I've left you labouring on my behalf. Yours, Thomas. On 07/02/13 02:38, Johannes Hölzl wrote: Am Mittwoch, den

[isabelle-dev] Problem with let-simproc

2013-02-05 Thread Johannes Hölzl
Hi Isabelle-dev, 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