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

Lawrence Paulson lp15 at cam.ac.uk
Tue Jan 14 15:13:59 CET 2014

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).


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.

More information about the isabelle-dev mailing list