src/HOL/Old_Datatype.thy
2014-09-11 blanchet 2014-09-11 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
2014-09-04 blanchet 2014-09-04 tweaked setup for datatype realizer
2014-09-03 blanchet 2014-09-03 moved old datatype material around
2014-09-01 blanchet 2014-09-01 renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place