src/HOL/Tools/value.ML
changeset 61442 467ebb937294
parent 59936 b8ffc3dc9e24
child 62969 9f394a16c557
equal deleted inserted replaced
61441:20ff1d5c74e1 61442:467ebb937294