# HG changeset patch
# User wenzelm
# Date 1169240884 -3600
# Node ID 7ee0529c56741a4b1fb39ac75e785f930f8be3c1
# Parent  fed088a475f9fc04bcf4e00e073b930212752ac5
renamed IsarOutput to ThyOutput;

diff -r fed088a475f9 -r 7ee0529c5674 doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Fri Jan 19 22:08:03 2007 +0100
+++ b/doc-src/TutorialI/Rules/Primes.thy	Fri Jan 19 22:08:04 2007 +0100
@@ -12,7 +12,7 @@
 
 
 ML "Pretty.setmargin 64"
-ML "IsarOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
+ML "ThyOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
 
 
 text {*Now in Basic.thy!
diff -r fed088a475f9 -r 7ee0529c5674 doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Fri Jan 19 22:08:03 2007 +0100
+++ b/doc-src/TutorialI/Types/Numbers.thy	Fri Jan 19 22:08:04 2007 +0100
@@ -2,7 +2,7 @@
 theory Numbers imports Real begin
 
 ML "Pretty.setmargin 64"
-ML "IsarOutput.indent := 0"  (*we don't want 5 for listing theorems*)
+ML "ThyOutput.indent := 0"  (*we don't want 5 for listing theorems*)
 
 text{*
 
diff -r fed088a475f9 -r 7ee0529c5674 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;