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
* More thorough check of proof context for goal statements and attributed
fact expressions: background theory, declared hyps, declared variable
names. Potential INCOMPATIBILITY, tools need to observe standard
context discipline.
This refers to Isabelle/f26a7f06266d.
It is a continuation of
* Activation of Z3 now works via z3_non_commercial system option
(without requiring restart), instead of former settings variable
Z3_NON_COMMERCIAL. The option can be edited in Isabelle/jEdit menu
Plugin Options / Isabelle / General.
This refers to Isabelle/0c07990363a3. For completeness, the
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
