[isabelle-dev] Safe approach to hypothesis substitution mark II

[Lawrence Paulson]

This sounds great! You seem to have done everything right.

Having the compatibility mode will make it easy to get everything working again quickly, with the conversion to the new setup becoming a background task (possibly to be combined with refactoring horrible old proofs).

Larry

On 14 Jan 2014, at 13:43, Thomas Sewell <Thomas.Sewell at nicta.com.au> wrote:

> For those reasons I'd prefer to plough ahead as long as the impact is manageable. I'll test the AFP and ISABELLE_FULL_TEST soon. I'm running out of energy for this side project, however. If there is some collection of proofs that are especially bad, we can just declare [[ hypsubst_thin = true ]] globally in them, but I hope to avoid that for the same reason as (2) above: having invisible adjustments to standard tactics seems like something we should avoid.