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

[Jasmin Christian Blanchette]

Hi Thomas,

Am 13.01.2014 um 13:38 schrieb Thomas Sewell <Thomas.Sewell at nicta.com.au>:

> The change requires, for instance, about a dozen lines of changes to the files in HOL/Library, which contain about 50K lines of proof, or 3 lines of changes to HOL/Bali, with 30K. The change to the Nominal examples (30K), however, is a bit longer (100 changes) and a bit more unpleasant. I've also checked the change against one chunk of L4.verified, with 70K lines in it, and have around 60 lines of changes to make. From my perspective, this level of impact seems to be annoying but not too annoying. I'm interested in what others think.

Your suggested change looks very reasonable to me. However, if possible, it would be nice if the old behavior could be kept via a flag -- unless it's easy to simulate reliably (e.g. using "thin_rl"). One reason for my concern is that the new (co)datatype package's tactics rely extensively on "hyp_subst_tac" and we currently don't have enough tests in the repository to catch all failures.

Cheers,

Jasmin