src/HOL/Tools/value_command.ML
changeset 74209 24a2a6ced0ab
parent 73761 ef1a18e20ace
child 74561 8e6c973003c8
equal deleted inserted replaced
74208:1a8d8dd77513 74209:24a2a6ced0ab