doc-src/TutorialI/settings.ML
author nipkow
Thu, 27 Oct 2011 16:28:34 +0200
changeset 45277 85b0ca9dd82f
parent 38767 d8da44a8dd25
permissions -rw-r--r--
uses IMP and hence requires its tex setup

Thy_Output.indent_default := 5;