src/Pure/deriv.ML
changeset 2183 8d42a7bccf0b
parent 2042 33b4c1624e26
child 2672 85d7e800d754
equal deleted inserted replaced
2182:29e56f003599 2183:8d42a7bccf0b