src/HOL/Datatype.ML
changeset 12847 afa356dbcb15
parent 11954 3d1780208bf3
child 12918 bca45be2d25b