src/HOL/Datatype.thy
changeset 17076 c7effdf2e2e2
parent 15140 322485b816ac
child 17458 e42bfad176eb