src/HOL/Tools/datatype_realizer.ML
changeset 80608 0b8922e351a3
parent 80295 8a9588ffc133