src/Pure/primitive_defs.ML
changeset 42581 398fff2c6b8f
parent 42284 326f57825e1a
child 44241 7943b69f0188
equal deleted inserted replaced
42580:04cae06f0b99 42581:398fff2c6b8f