[isabelle-dev] Status of recdef?
makarius at sketis.net
Sun Jul 24 17:05:03 CEST 2011
The old recdef package is another ancient duplicate that is mostly used in
old manuals now. Is there a scheme for eventual removal?
Since it is already marked as "legacy_feature" for quite some time, one
could move it to src/HOL/Library/Old_Recdef.thy, for example.
This would also reduce the ever-growing main HOL image a little bit. (I am
waiting for the day when Isabelle/HOL cannot be built on 32bit machines
with only 2GB anymore.)
More information about the isabelle-dev