Re: [isabelle] SELECT_GOAL and schematic variables
On Fri, 22 Mar 2013, Lawrence Paulson wrote:
I'm afraid that I really can't answer this question without a time
In principle the time machine is Mercurial, but it also takes time to
study our immense history that has accumulated since changeset 0 from
Sep-16 12:20:38 1993 (and more years of unwritten history before that).
The usual method of getting around such problems was to freeze variables
prior to applying the tactic, thawing them afterwards. That was a hack,
but it generally worked. My impression is that Makarius has replaced
such trickery by more robust methods, but it's possible that quite a lot
about old code is still there and running. I'm not sure about the
current best practice for dealing with this sort of situation.
The ancient freeze_thaw and freeze_thaw_robust (which were actually both
fragile) have evolved over a long way to become the current FOCUS
combinators, which are also mentioned in the "implementation" manual.
This Isar technology for structured tactic programming is useful in many
situations, but it does not really cover the schematic goal approach that
Peter appears to use a lot. In fact, the continued retreat of genuine
logic-programming with schematic variables in Isabelle tactics over the
years had paved the way for these more recent high-level tacticals.
Readers of the old "intro" manual by Larry might remember the final Prolog
example. Such techniques are now extremely rare, so it is no surprise
that certain tools choke.
(I will have a close look later at what is actually happening here, when I
have catched up with various other open threads.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and