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
On 29.01.2013 17:46, Lars Noschinski wrote:
On 28.11.2012 10:11, Lars Noschinski wrote:
Hi everyone,
mira still crashes from time to time.
I got a new one today.
lxbroy10 testboard `mira daemon 'bisect(Isabelle_makeall)'`
was hanging for more then 10 days in "Mirroring master repositories".
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
