src/Pure/deriv.ML
changeset 1868 836950047d85
parent 1601 0ef6ea27ab15
child 2042 33b4c1624e26