src/Pure/primitive_defs.ML
changeset 28054 2b84d34c5d02
parent 24981 4ec3f95190bf
child 29580 117b88da143c
equal deleted inserted replaced
28053:a2106c0d8c45 28054:2b84d34c5d02