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.

  -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.