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