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

Makarius makarius at sketis.net
Wed Jan 15 16:05:32 CET 2014

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 mailing list