src/HOL/Induct/QuoDataType.thy
changeset 40385 b70ef70733e8
parent 39910 10097e0a9dbd
child 40825 c55ee3793712