[isabelle-dev] Remaining uses of defer_recdef?
makarius at sketis.net
Thu Jun 11 15:51:01 CEST 2015
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
More information about the isabelle-dev