src/HOL/Induct/QuoDataType.thy
changeset 36811 4ab4aa5bee1c
parent 32960 69916a850301
child 39246 9e58f0499f57