[isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

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.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