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

Yours,
    Thomas.

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.


        Makarius
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to