[isabelle-dev] Remaining uses of defer_recdef?

Larry Paulson lp15 at cam.ac.uk
Sat Jun 6 01:13:17 CEST 2015

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.


> On 5 Jun 2015, at 21:42, Florian Haftmann <florian.haftmann at 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

More information about the isabelle-dev mailing list