src/HOL/Tools/value_command.ML
changeset 81092 c92efbf32bfe
parent 74561 8e6c973003c8
equal deleted inserted replaced
81091:c007e6d9941d 81092:c92efbf32bfe