src/HOL/Datatype.ML
changeset 11982 65e2822d83dd
parent 11954 3d1780208bf3
child 12918 bca45be2d25b