src/HOL/Induct/QuoDataType.thy
changeset 15165 a1e84e86c583
parent 15152 5c4d3f10ac5a
child 15169 2b5da07a0b89