src/HOL/Induct/QuoDataType.thy
changeset 39089 df379a447753
parent 32960 69916a850301
child 39246 9e58f0499f57