src/HOL/Datatype.ML
changeset 15130 dc6be28d7f4e
parent 14981 e73f8140af78
equal deleted inserted replaced
15129:fbf90acc5bf4 15130:dc6be28d7f4e