Whoops.
It's both a typo and use of the wrong release.
The patch happens to work against Isabelle2013-1 or Isabelle2013-2,
since there are no relevant differences in the theory sources. I can
confirm that isabelle build -a works in either 2013-1 or 2013-2.
Short version of the story, I forgo
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 wrote:
> On Tue, 14 Jan 2014, Thomas Sewell wrote:
>
>> If there is some collection of proofs that are esp
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 config
On Tue, 14 Jan 2014, Thomas Sewell wrote:
This is also a patch against Isabelle2013-1.
Is that just a typo, or are you still using that failed release? The
current one is Isabelle2013-2, and it does not introduce any
incompatibilities over Isabelle2013-1, so there is no reason to keep using
This sounds great! You seem to have done everything right.
Having the compatibility mode will make it easy to get everything working again
quickly, with the conversion to the new setup becoming a background task
(possibly to be combined with refactoring horrible old proofs).
Larry
On 14 Jan 20
Hi Thomas,
Am 14.01.2014 um 14:43 schrieb Thomas Sewell :
> To address Jasmin and Larry's concern, it is possible to switch back to the
> "compatibility mode" by setting a config variable in the context, or by
> calling the ML version with an extra parameter. Any legacy proof script can
> be r
Note that this change would affect auto, force, fast, etc.
Possibly a “legacy” version of auto would help with compatibility, or otherwise
some sort of option setting to (locally) restore the old behaviour in all
affected methods.
Larry
On 13 Jan 2014, at 15:47, Makarius wrote:
> With an eas
On Mon, 13 Jan 2014, Lawrence Paulson wrote:
I think the problem is that the unsafe situations cannot be detected
locally, i.e., there is no way for the tactic to know that a particular
free variable is actually a locale constant.
Indeed. The proposed change is basically some form of "locali
On Mon, 13 Jan 2014, Thomas Sewell wrote:
Given a hypothesis of the form "x = Suc a" or "Suc a = x", where x is a
free (blue) variable, hypsubst will substitute "Suc a" for x throughout
the goal, and then discard the hypothesis. The substitution is almost
always wanted. Discarding the hypothes
I’m impressed with your determination to slog through so many changes, but I am
not sure that we have the right to impose this on our users, which is why I
would prefer one of the other solutions, namely (1) contextual information if
available (2) some sort of compatibility mode.
Thank you very
I think the problem is that the unsafe situations cannot be detected locally,
i.e., there is no way for the tactic to know that a particular free variable is
actually a locale constant. I could be wrong: the current treatment of contexts
may make this information available after all. That would
> If there's interest in getting this change installed, I'll slog through
> these, and then figure out what's broken and what's expected to be broken in
> the latest tip of Isabelle and in the AFP. I'd call for volunteers to help
> with that bit though.
>
I would very much appreciate such a c
Hi Thomas,
Am 13.01.2014 um 13:38 schrieb Thomas Sewell :
> The change requires, for instance, about a dozen lines of changes to the
> files in HOL/Library, which contain about 50K lines of proof, or 3 lines of
> changes to HOL/Bali, with 30K. The change to the Nominal examples (30K),
> howeve
On Mon, 2014-01-13 at 12:38 +, Thomas Sewell wrote:
> Given a hypothesis of the form "x = Suc a" or "Suc a = x", where x is a
> free (blue) variable, hypsubst will substitute "Suc a" for x throughout
> the goal, and then discard the hypothesis. The substitution is almost
> always wanted. Discar
14 matches
Mail list logo