src/Tools/value.ML
changeset 29864 be53632b7f8d
parent 29288 253bcf2a5854
child 31218 fa54c1e614df
equal deleted inserted replaced
29863:dadad1831e9d 29864:be53632b7f8d