# HG changeset patch
# User wenzelm
# Date 1343661945 -7200
# Node ID b34ff75c23a73d8a57af628229f454752c87264d
# Parent  0095de9e9da0878f97a13f6b7b98785202a4ec22
multi-threaded HOL-Tutorial with explicit indication of local options;

diff -r 0095de9e9da0 -r b34ff75c23a7 doc-src/ROOT
--- a/doc-src/ROOT	Mon Jul 30 17:07:23 2012 +0200
+++ b/doc-src/ROOT	Mon Jul 30 17:25:45 2012 +0200
@@ -118,7 +118,7 @@
 session Tutorial (doc) in "TutorialI" = HOL +
   options [browser_info = false, document = false,
     document_dump = document, document_dump_mode = "tex",
-    print_mode = "brackets", threads = 1 (* FIXME *)]
+    print_mode = "brackets"]
   theories [thy_output_indent = 5]
     "ToyList/ToyList"
     "Ifexpr/Ifexpr"
@@ -157,7 +157,7 @@
     "Documents/Documents"
   theories [document_dump = ""]
     "Types/Setup"
-  theories
+  theories [pretty_margin = 64, thy_output_indent = 0]
     "Types/Numbers"
     "Types/Pairs"
     "Types/Records"
@@ -167,6 +167,8 @@
     "Rules/Basic"
     "Rules/Blast"
     "Rules/Force"
+  theories [pretty_margin = 64, thy_output_indent = 5]
+    "Rules/Primes"
     "Rules/Forward"
     "Rules/Tacticals"
     "Rules/find2"
diff -r 0095de9e9da0 -r b34ff75c23a7 doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Mon Jul 30 17:07:23 2012 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy	Mon Jul 30 17:25:45 2012 +0200
@@ -8,10 +8,6 @@
   "gcd m n = (if n=0 then m else gcd n (m mod n))"
 
 
-ML "Pretty.margin_default := 64"
-declare [[thy_output_indent = 5]]  (*that is, Doc/TutorialI/settings.ML*)
-
-
 text {*Now in Basic.thy!
 @{thm[display]"dvd_def"}
 \rulename{dvd_def}
diff -r 0095de9e9da0 -r b34ff75c23a7 doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Mon Jul 30 17:07:23 2012 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy	Mon Jul 30 17:25:45 2012 +0200
@@ -1,7 +1,6 @@
 theory Examples imports Main "~~/src/HOL/Library/Binomial" begin
 
 declare [[eta_contract = false]]
-ML "Pretty.margin_default := 64"
 
 text{*membership, intersection *}
 text{*difference and empty set*}
diff -r 0095de9e9da0 -r b34ff75c23a7 doc-src/TutorialI/Sets/Functions.thy
--- a/doc-src/TutorialI/Sets/Functions.thy	Mon Jul 30 17:07:23 2012 +0200
+++ b/doc-src/TutorialI/Sets/Functions.thy	Mon Jul 30 17:25:45 2012 +0200
@@ -1,7 +1,5 @@
 theory Functions imports Main begin
 
-ML "Pretty.margin_default := 64"
-
 
 text{*
 @{thm[display] id_def[no_vars]}
diff -r 0095de9e9da0 -r b34ff75c23a7 doc-src/TutorialI/Sets/Recur.thy
--- a/doc-src/TutorialI/Sets/Recur.thy	Mon Jul 30 17:07:23 2012 +0200
+++ b/doc-src/TutorialI/Sets/Recur.thy	Mon Jul 30 17:25:45 2012 +0200
@@ -1,7 +1,5 @@
 theory Recur imports Main begin
 
-ML "Pretty.margin_default := 64"
-
 
 text{*
 @{thm[display] mono_def[no_vars]}
diff -r 0095de9e9da0 -r b34ff75c23a7 doc-src/TutorialI/Sets/Relations.thy
--- a/doc-src/TutorialI/Sets/Relations.thy	Mon Jul 30 17:07:23 2012 +0200
+++ b/doc-src/TutorialI/Sets/Relations.thy	Mon Jul 30 17:25:45 2012 +0200
@@ -1,7 +1,5 @@
 theory Relations imports Main begin
 
-ML "Pretty.margin_default := 64"
-
 (*Id is only used in UNITY*)
 (*refl, antisym,trans,univalent,\<dots> ho hum*)
 
diff -r 0095de9e9da0 -r b34ff75c23a7 doc-src/TutorialI/Types/Numbers.thy
--- a/doc-src/TutorialI/Types/Numbers.thy	Mon Jul 30 17:07:23 2012 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Mon Jul 30 17:25:45 2012 +0200
@@ -2,9 +2,6 @@
 imports Complex_Main
 begin
 
-ML "Pretty.margin_default := 64"
-declare [[thy_output_indent = 0]]  (*we don't want 5 for listing theorems*)
-
 text{*
 
 numeric literals; default simprules; can re-orient
diff -r 0095de9e9da0 -r b34ff75c23a7 doc-src/TutorialI/document/Numbers.tex
--- a/doc-src/TutorialI/document/Numbers.tex	Mon Jul 30 17:07:23 2012 +0200
+++ b/doc-src/TutorialI/document/Numbers.tex	Mon Jul 30 17:25:45 2012 +0200
@@ -15,27 +15,9 @@
 {\isafoldtheory}%
 %
 \isadelimtheory
-\isanewline
 %
 \endisadelimtheory
 %
-\isadelimML
-\isanewline
-%
-\endisadelimML
-%
-\isatagML
-\isacommand{ML}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}Pretty{\isaliteral{2E}{\isachardot}}margin{\isaliteral{5F}{\isacharunderscore}}default\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{6}}{\isadigit{4}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-\isanewline
-%
-\endisadelimML
-\isacommand{declare}\isamarkupfalse%
-\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}thy{\isaliteral{5F}{\isacharunderscore}}output{\isaliteral{5F}{\isacharunderscore}}indent\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}%
 \begin{isamarkuptext}%
 numeric literals; default simprules; can re-orient%
 \end{isamarkuptext}%