src/HOL/Tools/datatype_realizer.ML
changeset 15131 c69542757a4d
parent 14981 e73f8140af78
child 15256 9237f388fbb1