src/Pure/deriv.ML
changeset 3538 ed9de44032e0
parent 2672 85d7e800d754
child 6085 3d8dcb09dbfb
equal deleted inserted replaced
3537:79ac9b475621 3538:ed9de44032e0