src/Pure/primitive_defs.ML
changeset 33528 b34511bbc121
parent 33385 fb2358edcfb6
child 35989 3418cdf1855e
equal deleted inserted replaced
33527:d4e5f6a40779 33528:b34511bbc121