src/Tools/value.ML
changeset 40338 e2f03de2b3c7
parent 37744 3daaf23b9ab4
child 42361 23f352990944
equal deleted inserted replaced
40337:d25bbb5f1c9e 40338:e2f03de2b3c7