# HG changeset patch
# User nipkow
# Date 968137397 -7200
# Node ID 109b11c4e77eaabf21f125a70c518e9fb9dbd6cc
# Parent  193dc80eaee9ba26840f5e58d2cab1fceeaf1a37
*** empty log message ***

diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/CodeGen/ROOT.ML
--- a/doc-src/TutorialI/CodeGen/ROOT.ML	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/CodeGen/ROOT.ML	Tue Sep 05 09:03:17 2000 +0200
@@ -1,1 +1,2 @@
+use "../settings.ML";
 use_thy "CodeGen";
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Datatype/Fundata.thy
--- a/doc-src/TutorialI/Datatype/Fundata.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -11,9 +11,7 @@
 @{typ"nat"}, we have an infinitely branching tree because each node
 has as many subtrees as there are natural numbers. How can we possibly
 write down such a tree? Using functional notation! For example, the term
-\begin{quote}
 @{term[display]"Branch 0 (%i. Branch i (%n. Tip))"}
-\end{quote}
 of type @{typ"(nat,nat)bigtree"} is the tree whose
 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
 has merely @{term"Tip"}s as further subtrees.
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Datatype/Nested.thy
--- a/doc-src/TutorialI/Datatype/Nested.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -76,9 +76,7 @@
 \begin{exercise}
 The fact that substitution distributes over composition can be expressed
 roughly as follows:
-\begin{quote}
 @{text[display]"subst (f o g) t = subst f (subst g t)"}
-\end{quote}
 Correct this statement (you will find that it does not type-check),
 strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
 its definition is found in theorem @{thm[source]o_def}).
@@ -92,9 +90,7 @@
 The experienced functional programmer may feel that our above definition of
 @{term"subst"} is unnecessarily complicated in that @{term"substs"} is
 completely unnecessary. The @{term"App"}-case can be defined directly as
-\begin{quote}
 @{term[display]"subst s (App f ts) = App f (map (subst s) ts)"}
-\end{quote}
 where @{term"map"} is the standard list function such that
 @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle
 insists on the above fixed format. Fortunately, we can easily \emph{prove}
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Datatype/ROOT.ML
--- a/doc-src/TutorialI/Datatype/ROOT.ML	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Datatype/ROOT.ML	Tue Sep 05 09:03:17 2000 +0200
@@ -1,3 +1,4 @@
+use "../settings.ML";
 use_thy "ABexpr";
 use_thy "unfoldnested";
 use_thy "Nested";
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Datatype/document/Fundata.tex
--- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Sep 05 09:03:17 2000 +0200
@@ -10,13 +10,11 @@
 \isa{nat}, we have an infinitely branching tree because each node
 has as many subtrees as there are natural numbers. How can we possibly
 write down such a tree? Using functional notation! For example, the term
-\begin{quote}
-
+%
 \begin{isabelle}%
-Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}
+\ \ \ \ \ Branch\ \isadigit{0}\ {\isacharparenleft}{\isasymlambda}i{\isachardot}\ Branch\ i\ {\isacharparenleft}{\isasymlambda}n{\isachardot}\ Tip{\isacharparenright}{\isacharparenright}%
 \end{isabelle}%
 
-\end{quote}
 of type \isa{{\isacharparenleft}nat{\isacharcomma}\ nat{\isacharparenright}\ bigtree} is the tree whose
 root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
 has merely \isa{Tip}s as further subtrees.
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Datatype/document/Nested.tex
--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Sep 05 09:03:17 2000 +0200
@@ -71,13 +71,11 @@
 \begin{exercise}
 The fact that substitution distributes over composition can be expressed
 roughly as follows:
-\begin{quote}
-
+%
 \begin{isabelle}%
-subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}
+\ \ \ \ \ subst\ {\isacharparenleft}f\ o\ g{\isacharparenright}\ t\ {\isacharequal}\ subst\ f\ {\isacharparenleft}subst\ g\ t{\isacharparenright}%
 \end{isabelle}%
 
-\end{quote}
 Correct this statement (you will find that it does not type-check),
 strengthen it, and prove it. (Note: \isaindexbold{o} is function composition;
 its definition is found in theorem \isa{o{\isacharunderscore}def}).
@@ -91,13 +89,11 @@
 The experienced functional programmer may feel that our above definition of
 \isa{subst} is unnecessarily complicated in that \isa{substs} is
 completely unnecessary. The \isa{App}-case can be defined directly as
-\begin{quote}
-
+%
 \begin{isabelle}%
-subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}
+\ \ \ \ \ subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}%
 \end{isabelle}%
 
-\end{quote}
 where \isa{map} is the standard list function such that
 \isa{map\ f\ {\isacharbrackleft}x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x\isadigit{1}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle
 insists on the above fixed format. Fortunately, we can easily \emph{prove}
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Ifexpr/ROOT.ML
--- a/doc-src/TutorialI/Ifexpr/ROOT.ML	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Ifexpr/ROOT.ML	Tue Sep 05 09:03:17 2000 +0200
@@ -1,1 +1,2 @@
+use "../settings.ML";
 use_thy "Ifexpr";
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Misc/AdvancedInd.thy
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -135,9 +135,7 @@
 usually known as ``mathematical induction''. There is also ``complete
 induction'', where you must prove $P(n)$ under the assumption that $P(m)$
 holds for all $m<n$. In Isabelle, this is the theorem @{thm[source]less_induct}:
-\begin{quote}
 @{thm[display]"less_induct"[no_vars]}
-\end{quote}
 Here is an example of its application.
 *};
 
@@ -267,9 +265,7 @@
 
 text{*\noindent
 The elimination rule @{thm[source]less_SucE} expresses the case distinction:
-\begin{quote}
 @{thm[display]"less_SucE"[no_vars]}
-\end{quote}
 
 Now it is straightforward to derive the original version of
 @{thm[source]less_induct} by manipulting the conclusion of the above lemma:
@@ -285,9 +281,7 @@
 text{*\noindent
 Finally we should mention that HOL already provides the mother of all
 inductions, \emph{wellfounded induction} (@{thm[source]wf_induct}):
-\begin{quote}
 @{thm[display]"wf_induct"[no_vars]}
-\end{quote}
 where @{term"wf r"} means that the relation @{term"r"} is wellfounded.
 For example @{thm[source]less_induct} is the special case where @{term"r"} is
 @{text"<"} on @{typ"nat"}. For details see the library.
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Misc/ROOT.ML
--- a/doc-src/TutorialI/Misc/ROOT.ML	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/ROOT.ML	Tue Sep 05 09:03:17 2000 +0200
@@ -1,3 +1,4 @@
+use "../settings.ML";
 use_thy "Tree";
 use_thy "Tree2";
 use_thy "case_exprs";
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Misc/case_exprs.thy
--- a/doc-src/TutorialI/Misc/case_exprs.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/case_exprs.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -7,9 +7,7 @@
 text{*\label{sec:case-expressions}
 HOL also features \isaindexbold{case}-expressions for analyzing
 elements of a datatype. For example,
-\begin{quote}
 @{term[display]"case xs of [] => 1 | y#ys => y"}
-\end{quote}
 evaluates to @{term"1"} if @{term"xs"} is @{term"[]"} and to @{term"y"} if 
 @{term"xs"} is @{term"y#ys"}. (Since the result in both branches must be of
 the same type, it follows that @{term"y"} is of type @{typ"nat"} and hence
@@ -34,15 +32,9 @@
 \noindent
 Nested patterns can be simulated by nested @{text"case"}-expressions: instead
 of
-% 
-\begin{quote}
-@{text"case xs of [] => 1 | [x] => x | x#(y#zs) => y"}
-%~~~case~xs~of~[]~{\isasymRightarrow}~1~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y
-\end{quote}
+@{text[display]"case xs of [] => 1 | [x] => x | x # (y # zs) => y"}
 write
-\begin{quote}
 @{term[display,eta_contract=false,margin=50]"case xs of [] => 1 | x#ys => (case ys of [] => x | y#zs => y)"}
-\end{quote}
 
 Note that @{text"case"}-expressions may need to be enclosed in parentheses to
 indicate their scope
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Sep 05 09:03:17 2000 +0200
@@ -120,13 +120,11 @@
 usually known as ``mathematical induction''. There is also ``complete
 induction'', where you must prove $P(n)$ under the assumption that $P(m)$
 holds for all $m<n$. In Isabelle, this is the theorem \isa{less{\isacharunderscore}induct}:
-\begin{quote}
-
+%
 \begin{isabelle}%
-{\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n
+\ \ \ \ \ {\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isasymforall}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymlongrightarrow}\ P\ m\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n%
 \end{isabelle}%
 
-\end{quote}
 Here is an example of its application.%
 \end{isamarkuptext}%
 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isacharequal}{\isachargreater}\ nat{\isachardoublequote}\isanewline
@@ -242,13 +240,11 @@
 \begin{isamarkuptext}%
 \noindent
 The elimination rule \isa{less{\isacharunderscore}SucE} expresses the case distinction:
-\begin{quote}
-
+%
 \begin{isabelle}%
-{\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P
+\ \ \ \ \ {\isasymlbrakk}m\ {\isacharless}\ Suc\ n{\isacharsemicolon}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P{\isacharsemicolon}\ m\ {\isacharequal}\ n\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P%
 \end{isabelle}%
 
-\end{quote}
 
 Now it is straightforward to derive the original version of
 \isa{less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:
@@ -263,13 +259,11 @@
 \noindent
 Finally we should mention that HOL already provides the mother of all
 inductions, \emph{wellfounded induction} (\isa{wf{\isacharunderscore}induct}):
-\begin{quote}
-
+%
 \begin{isabelle}%
-{\isasymlbrakk}wf\ r{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a
+\ \ \ \ \ {\isasymlbrakk}wf\ r{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}\ {\isasymin}\ r\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ a%
 \end{isabelle}%
 
-\end{quote}
 where \isa{wf\ r} means that the relation \isa{r} is wellfounded.
 For example \isa{less{\isacharunderscore}induct} is the special case where \isa{r} is
 \isa{{\isacharless}} on \isa{nat}. For details see the library.%
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Misc/document/case_exprs.tex
--- a/doc-src/TutorialI/Misc/document/case_exprs.tex	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/case_exprs.tex	Tue Sep 05 09:03:17 2000 +0200
@@ -7,13 +7,11 @@
 \label{sec:case-expressions}
 HOL also features \isaindexbold{case}-expressions for analyzing
 elements of a datatype. For example,
-\begin{quote}
-
+%
 \begin{isabelle}%
-case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y
+\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\ {\isacharbar}\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ y%
 \end{isabelle}%
 
-\end{quote}
 evaluates to \isa{\isadigit{1}} if \isa{xs} is \isa{{\isacharbrackleft}{\isacharbrackright}} and to \isa{y} if 
 \isa{xs} is \isa{y\ {\isacharhash}\ ys}. (Since the result in both branches must be of
 the same type, it follows that \isa{y} is of type \isa{nat} and hence
@@ -38,20 +36,18 @@
 \noindent
 Nested patterns can be simulated by nested \isa{case}-expressions: instead
 of
-% 
-\begin{quote}
-\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ \isadigit{1}\ {\isacharbar}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ x\ {\isacharbar}\ x{\isacharhash}{\isacharparenleft}y{\isacharhash}zs{\isacharparenright}\ {\isacharequal}{\isachargreater}\ y}
-%~~~case~xs~of~[]~{\isasymRightarrow}~1~|~[x]~{\isasymRightarrow}~x~|~x~\#~y~\#~zs~{\isasymRightarrow}~y
-\end{quote}
-write
-\begin{quote}
-
+%
 \begin{isabelle}%
-case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\isanewline
-{\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y
+\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ \isadigit{1}\ {\isacharbar}\ {\isacharbrackleft}x{\isacharbrackright}\ {\isacharequal}{\isachargreater}\ x\ {\isacharbar}\ x\ {\isacharhash}\ {\isacharparenleft}y\ {\isacharhash}\ zs{\isacharparenright}\ {\isacharequal}{\isachargreater}\ y%
 \end{isabelle}%
 
-\end{quote}
+write
+%
+\begin{isabelle}%
+\ \ \ \ \ case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ \isadigit{1}\isanewline
+\ \ \ \ \ {\isacharbar}\ x\ {\isacharhash}\ ys\ {\isasymRightarrow}\ case\ ys\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ x\ {\isacharbar}\ y\ {\isacharhash}\ zs\ {\isasymRightarrow}\ y%
+\end{isabelle}%
+
 
 Note that \isa{case}-expressions may need to be enclosed in parentheses to
 indicate their scope%
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Misc/document/natsum.tex
--- a/doc-src/TutorialI/Misc/document/natsum.tex	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/natsum.tex	Tue Sep 05 09:03:17 2000 +0200
@@ -4,13 +4,11 @@
 \begin{isamarkuptext}%
 \noindent
 In particular, there are \isa{case}-expressions, for example
-\begin{quote}
-
+%
 \begin{isabelle}%
-case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m
+\ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
 \end{isabelle}%
 
-\end{quote}
 primitive recursion, for example%
 \end{isamarkuptext}%
 \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Misc/natsum.thy
--- a/doc-src/TutorialI/Misc/natsum.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Misc/natsum.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -3,9 +3,7 @@
 (*>*)
 text{*\noindent
 In particular, there are @{text"case"}-expressions, for example
-\begin{quote}
 @{term[display]"case n of 0 => 0 | Suc m => m"}
-\end{quote}
 primitive recursion, for example
 *}
 
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Recdef/Nested1.thy
--- a/doc-src/TutorialI/Recdef/Nested1.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested1.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -22,9 +22,7 @@
 Remember that function @{term"size"} is defined for each \isacommand{datatype}.
 However, the definition does not succeed. Isabelle complains about an
 unproved termination condition
-\begin{quote}
 @{term[display]"t : set ts --> size t < Suc (term_list_size ts)"}
-\end{quote}
 where @{term"set"} returns the set of elements of a list (no special
 knowledge of sets is required in the following) and @{text"term_list_size ::
 term list \<Rightarrow> nat"} is an auxiliary function automatically defined by Isabelle
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Recdef/Nested2.thy
--- a/doc-src/TutorialI/Recdef/Nested2.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/Nested2.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -28,9 +28,7 @@
 apply(induct_tac t rule:trev.induct);
 txt{*\noindent
 This leaves us with a trivial base case @{term"trev (trev (Var x)) = Var x"} and the step case
-\begin{quote}
 @{term[display,margin=60]"ALL t. t : set ts --> trev (trev t) = t ==> trev (trev (App f ts)) = App f ts"}
-\end{quote}
 both of which are solved by simplification:
 *};
 
@@ -67,9 +65,7 @@
 (term_list_size ts)"}, without any assumption about @{term"t"}.  Therefore
 \isacommand{recdef} has been supplied with the congruence theorem
 @{thm[source]map_cong}:
-\begin{quote}
 @{thm[display,margin=50]"map_cong"[no_vars]}
-\end{quote}
 Its second premise expresses (indirectly) that the second argument of
 @{term"map"} is only applied to elements of its third argument. Congruence
 rules for other higher-order functions on lists would look very similar but
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Recdef/ROOT.ML
--- a/doc-src/TutorialI/Recdef/ROOT.ML	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/ROOT.ML	Tue Sep 05 09:03:17 2000 +0200
@@ -1,3 +1,4 @@
+use "../settings";
 use_thy "termination";
 use_thy "Induction";
 use_thy "Nested1";
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Recdef/document/Nested1.tex
--- a/doc-src/TutorialI/Recdef/document/Nested1.tex	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex	Tue Sep 05 09:03:17 2000 +0200
@@ -20,13 +20,11 @@
 Remember that function \isa{size} is defined for each \isacommand{datatype}.
 However, the definition does not succeed. Isabelle complains about an
 unproved termination condition
-\begin{quote}
-
+%
 \begin{isabelle}%
-t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}
+\ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
 \end{isabelle}%
 
-\end{quote}
 where \isa{set} returns the set of elements of a list (no special
 knowledge of sets is required in the following) and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary function automatically defined by Isabelle
 (when \isa{term} was defined).  First we have to understand why the
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Recdef/document/Nested2.tex
--- a/doc-src/TutorialI/Recdef/document/Nested2.tex	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested2.tex	Tue Sep 05 09:03:17 2000 +0200
@@ -22,14 +22,12 @@
 \begin{isamarkuptxt}%
 \noindent
 This leaves us with a trivial base case \isa{trev\ {\isacharparenleft}trev\ {\isacharparenleft}Var\ x{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ Var\ x} and the step case
-\begin{quote}
-
+%
 \begin{isabelle}%
-{\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline
-trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts
+\ \ \ \ \ {\isasymforall}t{\isachardot}\ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t\ {\isasymLongrightarrow}\isanewline
+\ \ \ \ \ trev\ {\isacharparenleft}trev\ {\isacharparenleft}App\ f\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ App\ f\ ts%
 \end{isabelle}%
 
-\end{quote}
 both of which are solved by simplification:%
 \end{isamarkuptxt}%
 \isacommand{by}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}rev{\isacharunderscore}map\ sym{\isacharbrackleft}OF\ map{\isacharunderscore}compose{\isacharbrackright}{\isacharparenright}%
@@ -64,14 +62,12 @@
 \isacommand{recdef} would try to prove the unprovable \isa{size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}}, without any assumption about \isa{t}.  Therefore
 \isacommand{recdef} has been supplied with the congruence theorem
 \isa{map{\isacharunderscore}cong}:
-\begin{quote}
-
+%
 \begin{isabelle}%
-{\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
-{\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys
+\ \ \ \ \ {\isasymlbrakk}xs\ {\isacharequal}\ ys{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ x\ {\isasymin}\ set\ ys\ {\isasymLongrightarrow}\ f\ x\ {\isacharequal}\ g\ x{\isasymrbrakk}\isanewline
+\ \ \ \ \ {\isasymLongrightarrow}\ map\ f\ xs\ {\isacharequal}\ map\ g\ ys%
 \end{isabelle}%
 
-\end{quote}
 Its second premise expresses (indirectly) that the second argument of
 \isa{map} is only applied to elements of its third argument. Congruence
 rules for other higher-order functions on lists would look very similar but
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Recdef/document/simplification.tex
--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Tue Sep 05 09:03:17 2000 +0200
@@ -16,13 +16,11 @@
 \noindent
 According to the measure function, the second argument should decrease with
 each recursive call. The resulting termination condition
-\begin{quote}
-
+%
 \begin{isabelle}%
-n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n
+\ \ \ \ \ n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
 \end{isabelle}%
 
-\end{quote}
 is provded automatically because it is already present as a lemma in the
 arithmetic library. Thus the recursion equation becomes a simplification
 rule. Of course the equation is nonterminating if we are allowed to unfold
@@ -31,29 +29,23 @@
 something else which leads to the same problem: it splits \isa{if}s if the
 condition simplifies to neither \isa{True} nor \isa{False}. For
 example, simplification reduces
-\begin{quote}
-
+%
 \begin{isabelle}%
-gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k
+\ \ \ \ \ gcd\ {\isacharparenleft}m{\isacharcomma}\ n{\isacharparenright}\ {\isacharequal}\ k%
 \end{isabelle}%
 
-\end{quote}
 in one step to
-\begin{quote}
-
+%
 \begin{isabelle}%
-{\isacharparenleft}if\ n\ {\isacharequal}\ \isadigit{0}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k
+\ \ \ \ \ {\isacharparenleft}if\ n\ {\isacharequal}\ \isadigit{0}\ then\ m\ else\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ k%
 \end{isabelle}%
 
-\end{quote}
 where the condition cannot be reduced further, and splitting leads to
-\begin{quote}
-
+%
 \begin{isabelle}%
-{\isacharparenleft}n\ {\isacharequal}\ \isadigit{0}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}
+\ \ \ \ \ {\isacharparenleft}n\ {\isacharequal}\ \isadigit{0}\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ k{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}n\ {\isasymnoteq}\ \isadigit{0}\ {\isasymlongrightarrow}\ gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}\ {\isacharequal}\ k{\isacharparenright}%
 \end{isabelle}%
 
-\end{quote}
 Since the recursive call \isa{gcd\ {\isacharparenleft}n{\isacharcomma}\ m\ mod\ n{\isacharparenright}} is no longer protected by
 an \isa{if}, it is unfolded again, which leads to an infinite chain of
 simplification steps. Fortunately, this problem can be avoided in many
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Recdef/simplification.thy
--- a/doc-src/TutorialI/Recdef/simplification.thy	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Tue Sep 05 09:03:17 2000 +0200
@@ -18,9 +18,7 @@
 text{*\noindent
 According to the measure function, the second argument should decrease with
 each recursive call. The resulting termination condition
-\begin{quote}
 @{term[display]"n ~= 0 ==> m mod n < n"}
-\end{quote}
 is provded automatically because it is already present as a lemma in the
 arithmetic library. Thus the recursion equation becomes a simplification
 rule. Of course the equation is nonterminating if we are allowed to unfold
@@ -29,17 +27,11 @@
 something else which leads to the same problem: it splits @{text"if"}s if the
 condition simplifies to neither @{term"True"} nor @{term"False"}. For
 example, simplification reduces
-\begin{quote}
 @{term[display]"gcd(m,n) = k"}
-\end{quote}
 in one step to
-\begin{quote}
 @{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
-\end{quote}
 where the condition cannot be reduced further, and splitting leads to
-\begin{quote}
 @{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
-\end{quote}
 Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
 an @{text"if"}, it is unfolded again, which leads to an infinite chain of
 simplification steps. Fortunately, this problem can be avoided in many
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/ToyList/ROOT.ML
--- a/doc-src/TutorialI/ToyList/ROOT.ML	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/ToyList/ROOT.ML	Tue Sep 05 09:03:17 2000 +0200
@@ -1,2 +1,3 @@
+use "../settings.ML";
 use_thy "ToyList";
 
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/Trie/ROOT.ML
--- a/doc-src/TutorialI/Trie/ROOT.ML	Mon Sep 04 21:20:14 2000 +0200
+++ b/doc-src/TutorialI/Trie/ROOT.ML	Tue Sep 05 09:03:17 2000 +0200
@@ -1,2 +1,3 @@
+use "../settings.ML";
 use_thy "Option2";
 use_thy "Trie";
diff -r 193dc80eaee9 -r 109b11c4e77e doc-src/TutorialI/settings.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/settings.ML	Tue Sep 05 09:03:17 2000 +0200
@@ -0,0 +1,1 @@
+IsarOutput.indent := 5;