src/HOL/Tools/datatype_realizer.ML
changeset 59153 b5e253703ebd
parent 59058 a78612c67ec0
child 59498 50b60f501b05