doc-src/TutorialI/settings.ML
author wenzelm
Fri, 16 Dec 2011 22:08:48 +0100
changeset 45902 4e70be32621a
parent 38767 d8da44a8dd25
permissions -rw-r--r--
more elementary defs;

Thy_Output.indent_default := 5;