src/HOL/Datatype.ML
changeset 12896 4518acda6d93
parent 11954 3d1780208bf3
child 12918 bca45be2d25b