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