Re: [isabelle] What replaces something specified as a legacy feature?



Such things are typically listed in the NEWS file in the root directory
of the Isabelle distribution. Changes that can break existing theories
are usually marked with INCOMPATIBILITY.

In my experience, such changes on the syntax level (such as the "legacy
name binding", which has been legacy since before I started learning
Isabelle around four years ago, if I am not mistaken) are relatively
rare. What happens more often is that some lemmas are changed or
renamed, breaking existing proofs. That appears in the NEWS file as
well. Everything in HOL and the AFP is normally ported by whoever
commits the breaking change; things outside HOL or the AFP will break
unless their maintainer updates them.

Changes that introduce significant incompatibilities like this are often
discussed on the mailing list in advance, to allow anyone who is
affected by them to voice their opinion on it.

More common, I think, are changes to ML code running in the background.
This usually only affects you if you directly interface with ML code
(e.g. writing own proof methods).

Manuel


On 09/04/15 09:28, W. Douglas Maurer wrote:
> I am trying to formalize the usual rule about checking whether a list
> is sorted by checking only adjacent elements of the list. So if t is
> an int list with no duplicate elements, then in order to show that t !
> i < t ! j for all i < j in range, it is enough to show that t ! i < t
> ! (i+1) for all i in range (other than the end of t, where t ! (i+1)
> is not defined). I wanted to formalize this with fixes, assumes, and
> shows, and so I started out by writing lemma fixes "t :: int list";
> and I got an error message reading Legacy feature! Bad name binding:
> "t :: int list". Well, if I understand the term "legacy feature," this
> is something that used to work, in older versions of Isabelle, so I
> must have learned it while using an older version. By experimentation
> I was able to get this to work by taking the "t :: " outside the
> double quotes, like this: lemma fixes t :: "int list" . But this
> raises a larger question: When features are taken out of Isabelle n in
> producing Isabelle n+1, is there a list of such features, somewhere,
> together with what they are replaced by? I don't want to teach my
> students something that no longer works, even if it used to work. I'm
> particularly interested in seeing such a list for Isabelle2015, when
> that comes out. -WDMaurer





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.