more compatibility between old- and new-style datatypes

added theory-based getters for convenience

made transfer functions slightly more general

tuned signatures

tuning

renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place

tuned structure inclusion

took out legacy material from 'HOL/Library/Library.thy'

removed commented out parts

tuned whitespace