[isabelle-dev] Remaining uses of defer_recdef?

[Thomas Sewell]

I've had a quick scan over the NICTA repositories. It doesn't look like
there are any live original uses of recdef. There are recdefs in a copy
of Simpl-AFP, and in some backups of historical papers.

Short summary, NICTA doesn't have any stakes in recdef.

Cheers,
     Thomas.

On 08/06/15 06:13, Makarius wrote:
> 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
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.