src/HOL/Tools/etc/options
changeset 75172 26ac98871d42
parent 74989 003f378b78a5
child 75412 b9c6758bb784