src/HOL/Tools/etc/settings
changeset 73255 7e2a9a8c2b85
parent 72218 a51736641843
child 73412 83569d243671