src/HOL/Tools/etc/options
changeset 81306 42b9bd119d2b
parent 80162 ccd76abeae1b
child 81529 92a3017f7d1a