[isabelle-dev] Remaining uses of defer_recdef?
makarius at sketis.net
Sat Jun 6 13:23:04 CEST 2015
On Sat, 6 Jun 2015, Larry Paulson wrote:
> I’d be happy to see the complete phasing out of TFL. It’s had its day.
> It was always a tricky thing to maintain. I’m amazed that it still works
> despite all of the many fundamental changes to system APIs.
There are actually two remaining parts of TFL:
(1) 'recdef' which is still used in Isabelle + AFP applications, but
very rarely and some effort could be made to get rid of it.
(2) 'defer_recdef' which is unused in the directly visible Isabelle
universe. So it could be deleted today.
This mailing list thread is an opportunity to point out dark matter in the
Isabelle universe, where 'defer_recdef' still occurs. Otherwise I will
remove it soon, lets say within 1-2 weeks.
Apart from that we should also work on (1) eventually. It has become a
ritual to ask about the purpose of old 'recdef', and it usually leads to
the result as "still needed" for odd reasons that I then forget
immediately. So I have developed a reluctance to ask again.
More information about the isabelle-dev