src/HOL/Datatype.ML
changeset 17771 1e07f6ab3118
parent 14981 e73f8140af78
equal deleted inserted replaced
17770:f13472d00645 17771:1e07f6ab3118