doc-src/TutorialI/settings.ML
author webertj
Mon, 07 Aug 2006 03:10:38 +0200
changeset 20346 b138816322c5
parent 9834 109b11c4e77e
child 22097 7ee0529c5674
permissions -rw-r--r--
title fixed

IsarOutput.indent := 5;