src/HOL/Tools/etc/options
changeset 81727 4ab59fef89ea
parent 81529 92a3017f7d1a
child 82024 bbda3b4f3c99