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



Dear Douglas,

In addition to what Manuel said, note that just because you can write something and get back the message "legacy feature" (thus assuming it was accepted in the past) it does not necessarily mean that the semantics is what you have in mind.

For your particular example I am suspecting (although I'm not a 100% sure) that

  fixes "t :: int list"

would have resulted in a fixed variable whose name is "t :: int list" (so not a variable called "t" of type "int list"). Not allowing this, is surely a good thing.

cheers

chris

On 04/09/2015 09:28 AM, 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.