src/Pure/deriv.ML
changeset 7707 1f4b67fdfdae
parent 6085 3d8dcb09dbfb