doc-src/TutorialI/settings.ML

--- a/doc-src/TutorialI/settings.ML	Fri Jan 19 22:08:03 2007 +0100
+++ b/doc-src/TutorialI/settings.ML	Fri Jan 19 22:08:04 2007 +0100
@@ -1,1 +1,3 @@
-IsarOutput.indent := 5;
+(* $Id$ *)
+
+ThyOutput.indent := 5;