src/HOL/Induct/QuoDataType.thy
changeset 61589 d07d0d5a572b
parent 61520 8f85bb443d33
child 63167 0909deb8059b