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 <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
