src/HOL/datatype.ML
changeset 1444 23ceb1dc9755
parent 1360 6bdee79ef125
child 1455 52a0271621f3