[isabelle-dev] Safe approach to hypothesis substitution
Thomas.Sewell at nicta.com.au
Thu Aug 26 03:19:32 CEST 2010
I'm pretty sure this one is a bug. Try typing this into your favourite
"fwrap f = (%v. f v) ==> P f"
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 to be safe, though, I can test this change in isolation against all
the HOL libraries and the AFP thisevening when my machine has spare CPU
time. I guess I should test against Isabelle 2009-2 rather than a
development snapshot since the AFP will be known to build?
On 26/08/10 02:49, Makarius wrote:
> 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 like
> that by some other tool.
> Anyway, I recommend to try that tiny bit of the change on all existing
> Isabelle + AFP theories. Then we can apply it independently, with a more
> informative log message that "fixed bug", though.
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
More information about the isabelle-dev