src/HOL/Datatype.thy
changeset 12791 ccc0f45ad2c4
parent 12029 7df1d840d01d
child 12918 bca45be2d25b