doc-src/TutorialI/settings.ML
author haftmann
Thu, 09 Aug 2007 15:52:53 +0200
changeset 24198 4031da6d8ba3
parent 22097 7ee0529c5674
child 37216 3165bc303f66
permissions -rw-r--r--
adaptions for code generation

(* $Id$ *)

ThyOutput.indent := 5;