On Thu, 11 Jun 2015, Larry Paulson wrote:
We must go forward and not back.
Just to conclude the original question on this thread: 'defer_recdef' is
unused, untested, unmaintained. So it falls under the normal
garbage-collection of source code. I will remove it next week or so,
unless there is another strong argument to keep it.
In contrast, the main 'recdef' is maintained a bit longer; of course
without any plans to "localize" it. Asymptotically, 'function' should
take over its role, but there is presently no attempt to change the
situation.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
