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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
