src/HOL/Induct/QuoDataType.thy
changeset 19510 29fc4e5a638c
parent 18460 9a1458cb2956
child 19736 d8d0f8f51d69