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 <makar...@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-...@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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
