src/Pure/primitive_defs.ML
changeset 35031 2ddc7edce107
parent 33385 fb2358edcfb6
child 35989 3418cdf1855e
equal deleted inserted replaced
35030:f2f1e50bf65d 35031:2ddc7edce107