src/HOL/Tools/value_command.ML
changeset 79718 fba02e281b44
parent 74561 8e6c973003c8
equal deleted inserted replaced
79717:da4e82434985 79718:fba02e281b44