src/ZF/Datatype.thy
changeset 524 b1bf18e83302
parent 516 1957113f0d7d
child 578 efc648d29dd0