src/HOL/Tools/etc/settings
changeset 83006 987cd5e21f72
parent 73987 fc363a3b690a