src/HOL/Datatype.ML
changeset 7360 7d3136b9af08
parent 7293 959e060f4a2f
child 9108 9fff97d29837