src/HOL/Datatype.thy
changeset 24261 dd31811bdf46
parent 24194 96013f81faef
child 24286 7619080e49f0