src/HOL/datatype.ML
changeset 4208 b67223fddc11
parent 4188 1025a27b08f9
child 4448 b587d40ad474
equal deleted inserted replaced
4207:061919f8da9c 4208:b67223fddc11