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
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
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
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
Hi Thomas,
Am 14.01.2014 um 14:43 schrieb Thomas Sewell thomas.sew...@nicta.com.au:
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
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
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. Discarding the
Hi Thomas,
Am 13.01.2014 um 13:38 schrieb Thomas Sewell thomas.sew...@nicta.com.au:
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
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
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
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
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
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 makar...@sketis.net
13 matches
Mail list logo
