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

Reply via email to