src/HOL/Tools/value_command.ML
changeset 65865 177b90f33f40
parent 63806 c54a53ef1873
child 66345 882abe912da9
equal deleted inserted replaced
65864:1945fa8f0c39 65865:177b90f33f40