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.
Larry > On 5 Jun 2015, at 21:42, Florian Haftmann > <florian.haftm...@informatik.tu-muenchen.de> wrote: > >> Cleaning up some obscure corners of the system, I've come across the old >> defer_recdef command. >> >> Are there any remaining uses of this historical relic? I don't see any >> in the main Isabelle repository + AFP. > > Some years ago the idea was to let recdef stand as long as there are > examples in the distribution. The consequence would be to dismantle > unused parts altogether. > > Further suggestios? > > Florian _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
