Re: [isabelle] Parallel proofs issue, potentially in subst method
On 12.09.2012 20:16, Makarius wrote:
I've had a quick look at the "subst" method, but it looks very bad. That
code has not been maintained in many years. It simply ignores the
all-important Proof.context when inventing free variables that are
expected to be fresh, but aren't. There is not just one place, but many.
One could probably make a small changeset to get your example working,
but it will then crash in another situation.
That is good to know. I have a student project planned (but no student
yet) to implement a subst-like tactic with the hole-selection of
ssreflects' rewrite tactic. I will keep in mind that subst's code is to
be taken with a grain of salt.
This archive was generated by a fusion of
Pipermail (Mailman edition) and