src/HOL/Induct/QuoDataType.thy
changeset 61373 16ed9b97c72d
parent 60530 44f9873d6f6f
child 61520 8f85bb443d33