src/HOL/Datatype.ML
changeset 15270 8b3f707a78a7
parent 14981 e73f8140af78
equal deleted inserted replaced
15269:f856f4f3258f 15270:8b3f707a78a7