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