[isabelle-dev] Status of recdef?

[Makarius]

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.)


 	Makarius