src/Pure/deriv.ML
changeset 8520 b6dd80ea3af1
parent 6085 3d8dcb09dbfb