Quoting Alexander Krauss kra...@in.tum.de:
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
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 problem.
