src/HOL/Tools/etc/options
changeset 58488 289d1c39968c
parent 57659 b246943b3aa3
child 59753 d743e0e53f41