src/HOL/datatype.ML
changeset 4987 257aeccdefc3
parent 4970 8b65444edbb0
equal deleted inserted replaced
4986:d4f257d3445a 4987:257aeccdefc3