Hi Thomas _Sewell_,
no no don't worry, the report was from Thomas _Tuerk_! And the change
was not too hard to produce.
What were your problems with the let-simproc? Did it to much or not
enough unfolding?
- Johannes
Am Donnerstag, den 07.02.2013, 11:34 +1100 schrieb Thomas Sewell:
> I'd forgot
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 06.02.20
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 Comple
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 [[
Okay, this fails in HOL-IMP.
The check I introduced is to strong. I relaxed the check now and it
should check if f =beta-eta-alpha= g, where g is the simplified version
of f.
The testboard changeset is:
http://isabelle.in.tum.de/testboard/Isabelle/rev/e9827a6f934e
- Johannes
Am Dienstag, 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 s
