src/HOL/Induct/QuoDataType.thy
changeset 41240 5965c8c97210
parent 40825 c55ee3793712
child 41959 b460124855b8