[isabelle-dev] Safe approach to hypothesis substitution mark II
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