src/Pure/deriv.ML
changeset 2250 891eb76b8045
parent 2042 33b4c1624e26
child 2672 85d7e800d754