src/HOL/Tools/datatype_realizer.ML
changeset 71042 400e9512f1d3
parent 70449 6e34025981be
child 74241 eb265f54e3ce