src/Pure/primitive_defs.ML
changeset 68129 b73678836f8e
parent 67721 5348bea4accd
child 74230 d637611b41bd
equal deleted inserted replaced
68128:4646124e683e 68129:b73678836f8e