src/Tools/value.ML
changeset 30368 1a2a54f910c9
parent 29288 253bcf2a5854
child 31218 fa54c1e614df
equal deleted inserted replaced
30367:ee8841b1b981 30368:1a2a54f910c9