[isabelle-dev] Remaining uses of defer_recdef?

[Makarius]

On Sat, 6 Jun 2015, Gerwin Klein wrote:

>
>> On 06.06.2015, at 21:23, Makarius <makarius at sketis.net> wrote:
>>
>>  (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.
>
> Unused in our part of the dark matter universe as well.

The thread has shifted over to actual 'recdef'. Are there remaining uses 
of 'recdef' in the NICTA dark matter?

So far I always thought the remaining uses in HOL-Decision_Procs are only 
a reminder that there are other important applications.


 	Makarius