src/HOL/Tools/etc/options
changeset 55633 460f4801b5cb
parent 55007 0c07990363a3
child 56623 4675df68450e