No doubt this is my responsibility, but this very complicated heap of code has
been out of my consciousness for many years. Sorting it out would be a
non-trivial project.
Larry
> On 30 Dec 2014, at 15:06, Makarius wrote:
>
> Metis proof reconstruction is already known to have occasional probl
Metis proof reconstruction is already known to have occasional problems
due to polymorphism. E.g. a long-pending question is how to avoid the
various workarounds for Thm.bicompose that can be seen in Brownian motion
here:
changeset: 52225:568b2cd65d50
user:wenzelm
date:Wed M
