src/HOL/Induct/QuoDataType.thy
changeset 40815 6e2d17cc0d1d
parent 39910 10097e0a9dbd
child 40825 c55ee3793712