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
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
