src/HOL/Datatype.ML
changeset 12791 ccc0f45ad2c4
parent 11954 3d1780208bf3
child 12918 bca45be2d25b