src/HOL/Datatype.thy
changeset 13846 b2c494d76012
parent 13635 c41e88151b54
child 14187 26dfcd0ac436