src/HOL/Tools/etc/settings
changeset 72239 12e94c2ff6c5
parent 72218 a51736641843
child 73412 83569d243671