src/HOL/Tools/datatype_realizer.ML
changeset 20328 5b240a4216b0
parent 20286 4cf8e86a2d29
child 21646 c07b5b0e8492