src/HOL/Datatype.ML
changeset 8364 0eb9ee70c8f8
parent 7293 959e060f4a2f
child 9108 9fff97d29837
equal deleted inserted replaced
8363:242dab4f164a 8364:0eb9ee70c8f8