src/HOL/datatype.ML
changeset 4447 b7ee449eb345
parent 4188 1025a27b08f9
child 4448 b587d40ad474
equal deleted inserted replaced
4446:097004a470fb 4447:b7ee449eb345