src/HOL/Induct/QuoDataType.thy
changeset 14722 8e739a6eaf11
parent 14658 b1293d0f8d5f
child 15120 f0359f75682e