src/HOL/Datatype.thy
changeset 28397 389c5e494605
parent 28346 b8390cd56b8f
child 28524 644b62cf678f