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