[isabelle-dev] Safe approach to hypothesis substitution mark II
lp15 at cam.ac.uk
Wed Jan 15 16:12:43 CET 2014
The name makes sense: thin refers to deleting the assumption.
It is ugly of course, which will be an incentive for users to update their proofs.
On 15 Jan 2014, at 15:05, Makarius <makarius at sketis.net> wrote:
> On Tue, 14 Jan 2014, Thomas Sewell wrote:
>> If there is some collection of proofs that are especially bad, we can just declare [[ hypsubst_thin = true ]]
> Larry, you are the original author of hypsubst.
> Does the "hypsubst_thin" terminology make sense to you? It is used here both for the configuration option and its attribute, and the alternate proof method that has it already enabled.
> For me it does make sense, i.e. we don't need to make it explicitly "legacy" in the wording.
More information about the isabelle-dev