src/HOL/Tools/etc/options
changeset 52861 e93d73b51fd0
parent 52717 da7bf8b3d24a
child 53057 e18a028b345c