doc-src/TutorialI/settings.ML
changeset 9834 109b11c4e77e
child 22097 7ee0529c5674
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/settings.ML	Tue Sep 05 09:03:17 2000 +0200
     1.3 @@ -0,0 +1,1 @@
     1.4 +IsarOutput.indent := 5;