renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place --HG-- rename : src/HOL/Datatype.thy => src/HOL/Old_Datatype.thy rename : src/HOL/Tools/Function/size.ML => src/HOL/Tools/Function/old_size.ML rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Old_Datatype/old_datatype.ML rename : src/HOL/Tools/Datatype/datatype_aux.ML => src/HOL/Tools/Old_Datatype/old_datatype_aux.ML rename : src/HOL/Tools/Datatype/datatype_codegen.ML => src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML rename : src/HOL/Tools/Datatype/datatype_data.ML => src/HOL/Tools/Old_Datatype/old_datatype_data.ML rename : src/HOL/Tools/Datatype/datatype_prop.ML => src/HOL/Tools/Old_Datatype/old_datatype_prop.ML rename : src/HOL/Tools/Datatype/datatype_realizer.ML => src/HOL/Tools/Old_Datatype/old_datatype_realizer.ML rename : src/HOL/Tools/Datatype/primrec.ML => src/HOL/Tools/Old_Datatype/old_primrec.ML rename : src/HOL/Tools/Datatype/rep_datatype.ML => src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
|