src/HOL/Induct/QuoNestedDataType.thy
changeset 21177 e8228486aa03
parent 20523 36a59e5d0039
child 21210 c17fd2df4e9e