--- 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"
--- 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}
--- 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*}
--- 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]}
--- 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]}
--- 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*)
--- 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
--- 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}%