src/Pure/primitive_defs.ML
changeset 38761 b32975d3db3e
parent 35989 3418cdf1855e
child 42284 326f57825e1a
equal deleted inserted replaced
38760:6f285436e3d6 38761:b32975d3db3e