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

[Lawrence Paulson]

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.

Larry

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