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



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
--
Prof. W. Douglas Maurer                Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University       Fax  (1-202)994-4875


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