src/HOL/Tools/etc/settings
changeset 72446 d189ad779a23
parent 72218 a51736641843
child 73412 83569d243671