Quoting Alexander Krauss :
The same can be done in low-level ML, using just "rtac", which
suggests that the error is somewhere in the underlying
Thm.biresolution etc. So far, I have not looked any further...
Hi Alex and Larry,
I guess the culprit is function rename_bvs in Pure/thm.ML, which
On 08/03/2011 12:34 PM, Lawrence Paulson wrote:
Many thanks for your analysis. It looks like an interaction involving "fix" and
bound variables.
Not too fast :-)
We must now peel off the various layers of Isar (recall that "show" is
just a normal refinement step), to get closer to the proble
