Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
renamed IsarOutput to ThyOutput;
authorwenzelm
Fri, 19 Jan 2007 22:08:04 +0100
changeset 22097 7ee0529c5674
parent 22096 fed088a475f9
child 22098 88be1b7775c8
renamed IsarOutput to ThyOutput;
doc-src/TutorialI/Rules/Primes.thy file | annotate | diff | comparison | revisions
doc-src/TutorialI/Types/Numbers.thy file | annotate | diff | comparison | revisions
doc-src/TutorialI/settings.ML file | annotate | diff | comparison | revisions 
--- 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!
--- 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{*
 
--- 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;
isabelle