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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
