src/HOL/Induct/QuoDataType.thy
changeset 80687 9b29c5d7aae4
parent 80067 c40bdfc84640
child 80914 d97fdabd9e2b
equal deleted inserted replaced
80686:dfafe46a37c4 80687:9b29c5d7aae4