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

[Makarius]

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