src/HOL/datatype.ML
changeset 4271 3a82492e70c5
parent 4188 1025a27b08f9
child 4448 b587d40ad474