src/HOL/Induct/QuoDataType.thy
changeset 45544 c0304794e9e4
parent 41959 b460124855b8
child 45694 4a8743618257