src/HOL/Tools/value_command.ML
changeset 66764 006deaf5c3dc
parent 66345 882abe912da9
child 67149 e61557884799