src/HOL/Tools/etc/options
changeset 82912 ad66fb23998a
parent 82825 5e9c9f2c2cd8