[isabelle-dev] Remaining uses of defer_recdef?

Thomas Sewell thomas.sewell at nicta.com.au
Tue Jun 9 03:27:07 CEST 2015

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.


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.

More information about the isabelle-dev mailing list