Now one could argue that since we need recdef, we should also keep the special variant defer_recdef, but if nobody speaks up for it, we don't have a proof that we really need it and it should go.
Tobias On 06/06/2015 13:23, Makarius wrote:
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. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
