Hi Thomas,
Thomas Sewell wrote:
It's interesting that my innocent thread on hypothesis substitution
has been hijacked into a discussion about context-aware coding
guidelines.
There is still hope if we move the unrelated discussions to another
thread...
I have another small comment on the
Let's try to answer everyone again:
Alex:
I think I was wrong about the cases involving algebra. There may be something
interesting going on. The prenormalisation phase calls clarify_tac, then
full_atomize_tac, then some other stuff. With a Free variable x assumed to be
even, the resulting
On Wed, 25 Aug 2010, Thomas Sewell wrote:
Finally, the change to inspect_pair is indeed just a bugfix. I don't
this check is needed for the simplifier driven version of hyp_subst
anyway, so the bug shouldn't often be seen.
Often it is hard to tell what is a bug or an obscure feature required
I'm pretty sure this one is a bug. Try typing this into your favourite
Isabelle session:
lemma foo:
fwrap f = (%v. f v) == P f
apply clarify
And note the system hangs. I think this is a pretty good argument to
support the case that it doesn't occur in any existing Isabelle scripts.
Just
