src/HOL/Tools/Datatype/datatype_data.ML
changeset 33970 74db95c74f89
parent 33969 1e7ca47c6c3d
child 34911 771830d3bd5e