As previously discussed in the thread "Safe for boolean equality", the
current strategy for using equality hypotheses 'x = expr', in which
substitution for x is done and then the hypothesis is discarded, is
unsafe. The conclusion of that discussion was that the problem was
annoying but fairly r
Hi Thomas,
Thanks for digging into this. The concrete patch is exactly what was
needed to advance this discussion. Here are a few comments. I am sure
others will have more...
I attach the resulting patch. After
several rounds of bugfixes and compatibility improvements, it requires
23 lines
Hello again isabelle-dev.
I should clear up some confusion that may have been caused by my mail. I was
trying to avoid repeating all that had been said on this issue, and it seems I
left out some that hadn't been said as well.
This approach avoids ever deleting an equality on a Free variable du
