[isabelle-dev] Safe approach to hypothesis substitution
makarius at sketis.net
Wed Aug 25 18:49:47 CEST 2010
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.
More information about the isabelle-dev