[isabelle-dev] Status of recdef?

Makarius 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 mailing list