src/HOL/Tools/datatype_package.ML
changeset 30223 24d975352879
parent 30201 39fefb3eedfc
child 30242 aea5d7fa7ef5
equal deleted inserted replaced
30222:4102bbf2af21 30223:24d975352879