src/HOL/Datatype.ML
changeset 17394 a8c9ed3f9818
parent 14981 e73f8140af78
equal deleted inserted replaced
17393:23b7e14ce640 17394:a8c9ed3f9818