src/Pure/deriv.ML
changeset 2840 7e03e61612b0
parent 2672 85d7e800d754
child 6085 3d8dcb09dbfb