src/HOL/Induct/QuoDataType.thy
changeset 14935 c2441592be14
parent 14658 b1293d0f8d5f
child 15120 f0359f75682e