# HG changeset patch
# User nipkow
# Date 980520628 -3600
# Node ID 59961d32b1ae0294990b6f54b00e328cf2503a26
# Parent  55c0f9a8df78119ed51beadd5c0942a1c2357ede
*** empty log message ***

diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/CTL/Base.thy
--- a/doc-src/TutorialI/CTL/Base.thy	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/Base.thy	Fri Jan 26 15:50:28 2001 +0100
@@ -60,7 +60,7 @@
 
 text{*\noindent
 Command \isacommand{typedecl} merely declares a new type but without
-defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
+defining it (see \S\ref{sec:typedecl}). Thus we know nothing
 about the type other than its existence. That is exactly what we need
 because @{typ state} really is an implicit parameter of our model.  Of
 course it would have been more generic to make @{typ state} a type
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Jan 26 15:50:28 2001 +0100
@@ -17,8 +17,9 @@
                   | AF formula;
 
 text{*\noindent
-which stands for "always in the future":
-on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
+which stands for ``\emph{A}lways in the \emph{F}uture'':
+on all infinite paths, at some point the formula holds.
+Formalizing the notion of an infinite path is easy
 in HOL: it is simply a function from @{typ nat} to @{typ state}.
 *};
 
@@ -67,7 +68,7 @@
 
 text{*\noindent
 Because @{term af} is monotone in its second argument (and also its first, but
-that is irrelevant) @{term"af A"} has a least fixed point:
+that is irrelevant), @{term"af A"} has a least fixed point:
 *};
 
 lemma mono_af: "mono(af A)";
@@ -150,8 +151,8 @@
 infinite @{term A}-avoiding path starting from @{term s}. The reason is
 that by unfolding @{term lfp} we find that if @{term s} is not in
 @{term"lfp(af A)"}, then @{term s} is not in @{term A} and there is a
-direct successor of @{term s} that is again not in @{term"lfp(af
-A)"}. Iterating this argument yields the promised infinite
+direct successor of @{term s} that is again not in \mbox{@{term"lfp(af
+A)"}}. Iterating this argument yields the promised infinite
 @{term A}-avoiding path. Let us formalize this sketch.
 
 The one-step argument in the sketch above
@@ -159,7 +160,7 @@
 *};
 
 lemma not_in_lfp_afD:
- "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t)\<in>M \<and> t \<notin> lfp(af A))";
+ "s \<notin> lfp(af A) \<Longrightarrow> s \<notin> A \<and> (\<exists> t. (s,t) \<in> M \<and> t \<notin> lfp(af A))";
 apply(erule contrapos_np);
 apply(rule ssubst[OF lfp_unfold[OF mono_af]]);
 apply(simp add:af_def);
@@ -196,8 +197,8 @@
    \<exists>p\<in>Paths s. \<forall>i. Q(p i)";
 
 txt{*\noindent
-First we rephrase the conclusion slightly because we need to prove both the path property
-and the fact that @{term Q} holds simultaneously:
+First we rephrase the conclusion slightly because we need to prove simultaneously
+both the path property and the fact that @{term Q} holds:
 *};
 
 apply(subgoal_tac "\<exists>p. s = p 0 \<and> (\<forall>i. (p i,p(i+1)) \<in> M \<and> Q(p i))");
@@ -216,7 +217,7 @@
 apply(clarsimp);
 
 txt{*\noindent
-After simplification and clarification the subgoal has the following compact form
+After simplification and clarification, the subgoal has the following form
 @{subgoals[display,indent=0,margin=70,goals_limit=1]}
 and invites a proof by induction on @{term i}:
 *};
@@ -225,7 +226,7 @@
  apply(simp);
 
 txt{*\noindent
-After simplification the base case boils down to
+After simplification, the base case boils down to
 @{subgoals[display,indent=0,margin=70,goals_limit=1]}
 The conclusion looks exceedingly trivial: after all, @{term t} is chosen such that @{prop"(s,t):M"}
 holds. However, we first have to show that such a @{term t} actually exists! This reasoning
@@ -345,8 +346,8 @@
 text{*
 
 The language defined above is not quite CTL\@. The latter also includes an
-until-operator @{term"EU f g"} with semantics ``there exists a path
-where @{term f} is true until @{term g} becomes true''. With the help
+until-operator @{term"EU f g"} with semantics ``there \emph{E}xists a path
+where @{term f} is true \emph{U}ntil @{term g} becomes true''. With the help
 of an auxiliary function
 *}
 
@@ -360,7 +361,7 @@
 
 text{*\noindent
 the semantics of @{term EU} is straightforward:
-@{text[display]"s \<Turnstile> EU f g = (\<exists>p. until A B s p)"}
+@{prop[display]"s \<Turnstile> EU f g = (\<exists>p. until {t. t \<Turnstile> f} {t. t \<Turnstile> g} s p)"}
 Note that @{term EU} is not definable in terms of the other operators!
 
 Model checking @{term EU} is again a least fixed point construction:
@@ -457,10 +458,10 @@
 It is clear that if all sets are finite, they can be represented as lists and the usual
 set operations are easily implemented. Only @{term lfp} requires a little thought.
 Fortunately, the HOL Library%
-\footnote{See theory \isa{While_Combinator_Example}.}
+\footnote{See theory \isa{While_Combinator}.}
 provides a theorem stating that 
 in the case of finite sets and a monotone function~@{term F},
-the value of @{term"lfp F"} can be computed by iterated application of @{term F} to~@{term"{}"} until
+the value of \mbox{@{term"lfp F"}} can be computed by iterated application of @{term F} to~@{term"{}"} until
 a fixed point is reached. It is actually possible to generate executable functional programs
 from HOL definitions, but that is beyond the scope of the tutorial.
 *}
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/CTL/PDL.thy
--- a/doc-src/TutorialI/CTL/PDL.thy	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/PDL.thy	Fri Jan 26 15:50:28 2001 +0100
@@ -42,8 +42,8 @@
 
 text{*\noindent
 The first three equations should be self-explanatory. The temporal formula
-@{term"AX f"} means that @{term f} is true in all next states whereas
-@{term"EF f"} means that there exists some future state in which @{term f} is
+@{term"AX f"} means that @{term f} is true in \emph{A}ll ne\emph{X}t states whereas
+@{term"EF f"} means that there \emph{E}xists some \emph{F}uture state in which @{term f} is
 true. The future is expressed via @{text"\<^sup>*"}, the reflexive transitive
 closure. Because of reflexivity, the future includes the present.
 
@@ -68,7 +68,7 @@
 fixed point (@{term lfp}) of @{term"\<lambda>T. mc f \<union> M\<inverse> `` T"} is the least set
 @{term T} containing @{term"mc f"} and all predecessors of @{term T}. If you
 find it hard to see that @{term"mc(EF f)"} contains exactly those states from
-which there is a path to a state where @{term f} is true, do not worry --- that
+which there is a path to a state where @{term f} is true, do not worry --- this
 will be proved in a moment.
 
 First we prove monotonicity of the function inside @{term lfp}
@@ -180,7 +180,7 @@
 text{*
 \begin{exercise}
 @{term AX} has a dual operator @{term EN}\footnote{We cannot use the customary @{text EX}
-as that is the ASCII equivalent of @{text"\<exists>"}}
+as that is the \textsc{ascii}-equivalent of @{text"\<exists>"}}
 (``there exists a next state such that'') with the intended semantics
 @{prop[display]"(s \<Turnstile> EN f) = (EX t. (s,t) : M & t \<Turnstile> f)"}
 Fortunately, @{term"EN f"} can already be expressed as a PDL formula. How?
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/CTL/document/Base.tex
--- a/doc-src/TutorialI/CTL/document/Base.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/Base.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -63,7 +63,7 @@
 \begin{isamarkuptext}%
 \noindent
 Command \isacommand{typedecl} merely declares a new type but without
-defining it (see also \S\ref{sec:typedecl}). Thus we know nothing
+defining it (see \S\ref{sec:typedecl}). Thus we know nothing
 about the type other than its existence. That is exactly what we need
 because \isa{state} really is an implicit parameter of our model.  Of
 course it would have been more generic to make \isa{state} a type
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/CTL/document/CTL.tex
--- a/doc-src/TutorialI/CTL/document/CTL.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -15,8 +15,9 @@
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ AF\ formula%
 \begin{isamarkuptext}%
 \noindent
-which stands for "always in the future":
-on all paths, at some point the formula holds. Formalizing the notion of an infinite path is easy
+which stands for ``\emph{A}lways in the \emph{F}uture'':
+on all infinite paths, at some point the formula holds.
+Formalizing the notion of an infinite path is easy
 in HOL: it is simply a function from \isa{nat} to \isa{state}.%
 \end{isamarkuptext}%
 \isacommand{constdefs}\ Paths\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ state{\isacharparenright}set{\isachardoublequote}\isanewline
@@ -45,7 +46,7 @@
 \begin{isamarkuptext}%
 \noindent
 Because \isa{af} is monotone in its second argument (and also its first, but
-that is irrelevant) \isa{af\ A} has a least fixed point:%
+that is irrelevant), \isa{af\ A} has a least fixed point:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ mono{\isacharunderscore}af{\isacharcolon}\ {\isachardoublequote}mono{\isacharparenleft}af\ A{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ mono{\isacharunderscore}def\ af{\isacharunderscore}def{\isacharparenright}\isanewline
@@ -111,14 +112,14 @@
 infinite \isa{A}-avoiding path starting from \isa{s}. The reason is
 that by unfolding \isa{lfp} we find that if \isa{s} is not in
 \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}, then \isa{s} is not in \isa{A} and there is a
-direct successor of \isa{s} that is again not in \isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}. Iterating this argument yields the promised infinite
+direct successor of \isa{s} that is again not in \mbox{\isa{lfp\ {\isacharparenleft}af\ A{\isacharparenright}}}. Iterating this argument yields the promised infinite
 \isa{A}-avoiding path. Let us formalize this sketch.
 
 The one-step argument in the sketch above
 is proved by a variant of contraposition:%
 \end{isamarkuptext}%
 \isacommand{lemma}\ not{\isacharunderscore}in{\isacharunderscore}lfp{\isacharunderscore}afD{\isacharcolon}\isanewline
-\ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}{\isasymin}M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
+\ {\isachardoublequote}s\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}\ {\isasymLongrightarrow}\ s\ {\isasymnotin}\ A\ {\isasymand}\ {\isacharparenleft}{\isasymexists}\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymnotin}\ lfp{\isacharparenleft}af\ A{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isanewline
 \isacommand{apply}{\isacharparenleft}erule\ contrapos{\isacharunderscore}np{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}rule\ ssubst{\isacharbrackleft}OF\ lfp{\isacharunderscore}unfold{\isacharbrackleft}OF\ mono{\isacharunderscore}af{\isacharbrackright}{\isacharbrackright}{\isacharparenright}\isanewline
 \isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}af{\isacharunderscore}def{\isacharparenright}\isanewline
@@ -153,8 +154,8 @@
 \ \ \ {\isasymexists}p{\isasymin}Paths\ s{\isachardot}\ {\isasymforall}i{\isachardot}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptxt}%
 \noindent
-First we rephrase the conclusion slightly because we need to prove both the path property
-and the fact that \isa{Q} holds simultaneously:%
+First we rephrase the conclusion slightly because we need to prove simultaneously
+both the path property and the fact that \isa{Q} holds:%
 \end{isamarkuptxt}%
 \isacommand{apply}{\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequote}{\isasymexists}p{\isachardot}\ s\ {\isacharequal}\ p\ {\isadigit{0}}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}i{\isachardot}\ {\isacharparenleft}p\ i{\isacharcomma}p{\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q{\isacharparenleft}p\ i{\isacharparenright}{\isacharparenright}{\isachardoublequote}{\isacharparenright}%
 \begin{isamarkuptxt}%
@@ -170,7 +171,7 @@
 \isacommand{apply}{\isacharparenleft}clarsimp{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
-After simplification and clarification the subgoal has the following compact form
+After simplification and clarification, the subgoal has the following form
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline
 \isaindent{\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}i{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}path\ s\ Q\ i{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\isanewline
@@ -182,7 +183,7 @@
 \ \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}%
 \begin{isamarkuptxt}%
 \noindent
-After simplification the base case boils down to
+After simplification, the base case boils down to
 \begin{isabelle}%
 \ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}Q\ s{\isacharsemicolon}\ {\isasymforall}s{\isachardot}\ Q\ s\ {\isasymlongrightarrow}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}{\isasymrbrakk}\isanewline
 \isaindent{\ {\isadigit{1}}{\isachardot}\ }{\isasymLongrightarrow}\ {\isacharparenleft}s{\isacharcomma}\ SOME\ t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ Q\ t{\isacharparenright}\ {\isasymin}\ M%
@@ -281,8 +282,8 @@
 \isacommand{done}%
 \begin{isamarkuptext}%
 The language defined above is not quite CTL\@. The latter also includes an
-until-operator \isa{EU\ f\ g} with semantics ``there exists a path
-where \isa{f} is true until \isa{g} becomes true''. With the help
+until-operator \isa{EU\ f\ g} with semantics ``there \emph{E}xists a path
+where \isa{f} is true \emph{U}ntil \isa{g} becomes true''. With the help
 of an auxiliary function%
 \end{isamarkuptext}%
 \isacommand{consts}\ until{\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ set\ {\isasymRightarrow}\ state\ set\ {\isasymRightarrow}\ state\ {\isasymRightarrow}\ state\ list\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
@@ -293,7 +294,7 @@
 \noindent
 the semantics of \isa{EU} is straightforward:
 \begin{isabelle}%
-\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ A\ B\ s\ p{\isacharparenright}%
+\ \ \ \ \ s\ {\isasymTurnstile}\ EU\ f\ g\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}p{\isachardot}\ until\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ f{\isacharbraceright}\ {\isacharbraceleft}t{\isachardot}\ t\ {\isasymTurnstile}\ g{\isacharbraceright}\ s\ p{\isacharparenright}%
 \end{isabelle}
 Note that \isa{EU} is not definable in terms of the other operators!
 
@@ -320,10 +321,10 @@
 It is clear that if all sets are finite, they can be represented as lists and the usual
 set operations are easily implemented. Only \isa{lfp} requires a little thought.
 Fortunately, the HOL Library%
-\footnote{See theory \isa{While_Combinator_Example}.}
+\footnote{See theory \isa{While_Combinator}.}
 provides a theorem stating that 
 in the case of finite sets and a monotone function~\isa{F},
-the value of \isa{lfp\ F} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
+the value of \mbox{\isa{lfp\ F}} can be computed by iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until
 a fixed point is reached. It is actually possible to generate executable functional programs
 from HOL definitions, but that is beyond the scope of the tutorial.%
 \end{isamarkuptext}%
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/CTL/document/PDL.tex
--- a/doc-src/TutorialI/CTL/document/PDL.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/PDL.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -43,8 +43,8 @@
 \begin{isamarkuptext}%
 \noindent
 The first three equations should be self-explanatory. The temporal formula
-\isa{AX\ f} means that \isa{f} is true in all next states whereas
-\isa{EF\ f} means that there exists some future state in which \isa{f} is
+\isa{AX\ f} means that \isa{f} is true in \emph{A}ll ne\emph{X}t states whereas
+\isa{EF\ f} means that there \emph{E}xists some \emph{F}uture state in which \isa{f} is
 true. The future is expressed via \isa{\isactrlsup {\isacharasterisk}}, the reflexive transitive
 closure. Because of reflexivity, the future includes the present.
 
@@ -68,7 +68,7 @@
 fixed point (\isa{lfp}) of \isa{{\isasymlambda}T{\isachardot}\ mc\ f\ {\isasymunion}\ M{\isasyminverse}\ {\isacharbackquote}{\isacharbackquote}\ T} is the least set
 \isa{T} containing \isa{mc\ f} and all predecessors of \isa{T}. If you
 find it hard to see that \isa{mc\ {\isacharparenleft}EF\ f{\isacharparenright}} contains exactly those states from
-which there is a path to a state where \isa{f} is true, do not worry --- that
+which there is a path to a state where \isa{f} is true, do not worry --- this
 will be proved in a moment.
 
 First we prove monotonicity of the function inside \isa{lfp}
@@ -177,7 +177,7 @@
 \begin{isamarkuptext}%
 \begin{exercise}
 \isa{AX} has a dual operator \isa{EN}\footnote{We cannot use the customary \isa{EX}
-as that is the ASCII equivalent of \isa{{\isasymexists}}}
+as that is the \textsc{ascii}-equivalent of \isa{{\isasymexists}}}
 (``there exists a next state such that'') with the intended semantics
 \begin{isabelle}%
 \ \ \ \ \ s\ {\isasymTurnstile}\ EN\ f\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}t{\isachardot}\ {\isacharparenleft}s{\isacharcomma}\ t{\isacharparenright}\ {\isasymin}\ M\ {\isasymand}\ t\ {\isasymTurnstile}\ f{\isacharparenright}%
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/Misc/document/simp.tex
--- a/doc-src/TutorialI/Misc/document/simp.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -166,7 +166,7 @@
 Of course we can also unfold definitions in the middle of a proof.
 
 You should normally not turn a definition permanently into a simplification
-rule because this defeats the whole purpose of an abbreviation.
+rule because this defeats the whole purpose.
 
 \begin{warn}
   If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/Misc/simp.thy
--- a/doc-src/TutorialI/Misc/simp.thy	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy	Fri Jan 26 15:50:28 2001 +0100
@@ -162,7 +162,7 @@
 Of course we can also unfold definitions in the middle of a proof.
 
 You should normally not turn a definition permanently into a simplification
-rule because this defeats the whole purpose of an abbreviation.
+rule because this defeats the whole purpose.
 
 \begin{warn}
   If you have defined $f\,x\,y~\isasymequiv~t$ then you can only unfold
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -966,7 +966,7 @@
 
 \subsection{Definite Descriptions}
 
-In ASCII, we write \isa{SOME} for $\varepsilon$.
+In \textsc{ascii}, we write \isa{SOME} for $\varepsilon$.
 \REMARK{the internal constant is \isa{Eps}}
 The main use of \hbox{\isa{SOME\ x.\ P\ x}} is as a \textbf{definite
 description}: when \isa{P} is satisfied by a unique value,~\isa{a}. 
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/Sets/Functions.thy
--- a/doc-src/TutorialI/Sets/Functions.thy	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Sets/Functions.thy	Fri Jan 26 15:50:28 2001 +0100
@@ -79,7 +79,7 @@
 *}
 
 lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
-  apply (simp add: expand_fun_eq inj_on_def o_def)
+  apply (simp add: expand_fun_eq inj_on_def)
   apply (auto)
   done
 
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -96,7 +96,7 @@
 \isacommand{by}\ blast
 \end{isabelle}
 %
-This is the same example using ASCII syntax, illustrating a pitfall: 
+This is the same example using \textsc{ascii} syntax, illustrating a pitfall: 
 \begin{isabelle}
 \isacommand{lemma}\ "(A\ <=\ -B)\ =\ (B\ <=\ -A)"
 \end{isabelle}
@@ -287,8 +287,8 @@
 \end{isabelle}
 
 Unions can be formed over the values of a given  set.  The syntax is
-\isa{\isasymUnion x\isasymin A.\ B} or \isa{UN
-x:\ A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
+\mbox{\isa{\isasymUnion x\isasymin A.\ B}} or \isa{UN
+x\isasymin A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
 \begin{isabelle}
 (b\ \isasymin\
 (\isasymUnion x\isasymin A.\ B\ x))\ =\ (\isasymexists x\isasymin A.\
@@ -320,12 +320,12 @@
 over a \emph{type}:
 \begin{isabelle}
 \ \ \ \ \
-({\isasymUnion}x.\ B\ x)\ {==}\
+({\isasymUnion}x.\ B\ x)\ {\isasymrightleftharpoons}\
 ({\isasymUnion}x{\isasymin}UNIV.\ B\ x)
 \end{isabelle}
 Abbreviations work as you might expect.  The term on the left-hand side of
 the
-\isa{==} symbol is automatically translated to the right-hand side when the
+\indexboldpos{\isasymrightleftharpoons}{$IsaEqq} symbol is automatically translated to the right-hand side when the
 term is parsed, the reverse translation being done when the term is
 displayed.
 
@@ -523,7 +523,7 @@
 
 Theorems involving these concepts can be hard to prove. The following 
 example is easy, but it cannot be proved automatically. To begin 
-with, we need a law that relates the quality of functions to 
+with, we need a law that relates the equality of functions to 
 equality over all arguments: 
 \begin{isabelle}
 (f\ =\ g)\ =\ ({\isasymforall}x.\ f\ x\ =\ g\ x)
@@ -535,7 +535,7 @@
 side of function composition: 
 \begin{isabelle}
 \isacommand{lemma}\ "inj\ f\ \isasymLongrightarrow\ (f\ o\ g\ =\ f\ o\ h)\ =\ (g\ =\ h)"\isanewline
-\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def\ o_def)\isanewline
+\isacommand{apply}\ (simp\ add:\ expand_fun_eq\ inj_on_def)\isanewline
 \isacommand{apply}\ auto\isanewline
 \isacommand{done}
 \end{isabelle}
@@ -593,7 +593,7 @@
 abbreviates an application of image to {\isa{UNIV}}: 
 \begin{isabelle}
 \ \ \ \ \ range\ f\
-{==}\ f`UNIV
+{\isasymrightleftharpoons}\ f`UNIV
 \end{isabelle}
 %
 Few theorems are proved specifically 
@@ -845,7 +845,7 @@
 Induction comes in many forms, including traditional mathematical 
 induction, structural induction on lists and induction on size. 
 More general than these is induction over a well-founded relation. 
-Such A relation expresses the notion of a terminating process. 
+Such a relation expresses the notion of a terminating process. 
 Intuitively, the relation~$\prec$ is \textbf{well-founded} if it admits no
 infinite  descending chains
 \[ \cdots \prec a@2 \prec a@1 \prec a@0. \]
@@ -944,9 +944,9 @@
 
 \section{Fixed Point Operators}
 
-Fixed point operators define sets recursively.  Most users invoke 
-them by making an inductive definition, as discussed in
-Chap.\ts\ref{chap:inductive} below.  However, they can be used directly.
+Fixed point operators define sets recursively.  They are invoked
+implicitly when making an inductive definition, as discussed in
+Chap.\ts\ref{chap:inductive} below.  However, they can be used directly, too.
 The
 \relax{least}  or \relax{strongest} fixed point yields an inductive
 definition;  the \relax{greatest} or \relax{weakest} fixed point yields a
@@ -954,7 +954,7 @@
 existence  of these fixed points is guaranteed by the Knaster-Tarski
 theorem. 
 
-The theory works applies only to monotonic functions. Isabelle's 
+The theory applies only to monotonic functions. Isabelle's 
 definition of monotone is overloaded over all orderings:
 \begin{isabelle}
 mono\ f\ \isasymequiv\ {\isasymforall}A\ B.\ A\ \isasymle\ B\ \isasymlongrightarrow\ f\ A\ \isasymle\ f\ B%
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/Types/Typedef.thy
--- a/doc-src/TutorialI/Types/Typedef.thy	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Types/Typedef.thy	Fri Jan 26 15:50:28 2001 +0100
@@ -96,8 +96,10 @@
 @{term Abs_three} &::& @{typ"nat \<Rightarrow> three"}
 \end{tabular}
 \end{center}
-Constant @{term three} is just an abbreviation (@{thm[source]three_def}):
-@{thm[display]three_def}
+Constant @{term three} is explicitly defined as the representing set:
+\begin{center}
+@{thm three_def}\hfill(@{thm[source]three_def})
+\end{center}
 The situation is best summarized with the help of the following diagram,
 where squares are types and circles are sets:
 \begin{center}
@@ -118,10 +120,10 @@
 surjective on the subset @{term three} and @{term Abs_three} and @{term
 Rep_three} are inverses of each other:
 \begin{center}
-\begin{tabular}{rl}
-@{thm Rep_three[no_vars]} &~~ (@{thm[source]Rep_three}) \\
-@{thm Rep_three_inverse[no_vars]} &~~ (@{thm[source]Rep_three_inverse}) \\
-@{thm Abs_three_inverse[no_vars]} &~~ (@{thm[source]Abs_three_inverse})
+\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
+@{thm Rep_three[no_vars]} & (@{thm[source]Rep_three}) \\
+@{thm Rep_three_inverse[no_vars]} & (@{thm[source]Rep_three_inverse}) \\
+@{thm Abs_three_inverse[no_vars]} & (@{thm[source]Abs_three_inverse})
 \end{tabular}
 \end{center}
 %
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/Types/document/Typedef.tex
--- a/doc-src/TutorialI/Types/document/Typedef.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Typedef.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -102,10 +102,10 @@
 \isa{Abs{\isacharunderscore}three} &::& \isa{nat\ {\isasymRightarrow}\ three}
 \end{tabular}
 \end{center}
-Constant \isa{three} is just an abbreviation (\isa{three{\isacharunderscore}def}):
-\begin{isabelle}%
-three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}%
-\end{isabelle}
+Constant \isa{three} is explicitly defined as the representing set:
+\begin{center}
+\isa{three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def})
+\end{center}
 The situation is best summarized with the help of the following diagram,
 where squares are types and circles are sets:
 \begin{center}
@@ -125,10 +125,10 @@
 Finally, \isacommand{typedef} asserts that \isa{Rep{\isacharunderscore}three} is
 surjective on the subset \isa{three} and \isa{Abs{\isacharunderscore}three} and \isa{Rep{\isacharunderscore}three} are inverses of each other:
 \begin{center}
-\begin{tabular}{rl}
-\isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} &~~ (\isa{Rep{\isacharunderscore}three}) \\
-\isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} &~~ (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\
-\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} &~~ (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse})
+\begin{tabular}{@ {}r@ {\qquad\qquad}l@ {}}
+\isa{Rep{\isacharunderscore}three\ x\ {\isasymin}\ three} & (\isa{Rep{\isacharunderscore}three}) \\
+\isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}\ {\isacharequal}\ x} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inverse}) \\
+\isa{y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ y} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inverse})
 \end{tabular}
 \end{center}
 %
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/Types/numerics.tex
--- a/doc-src/TutorialI/Types/numerics.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -270,7 +270,7 @@
 
 \begin{warn}
 The absolute value bars shown above cannot be typed on a keyboard.  They
-can be entered using the X-symbol package.  In ASCII, type \isa{abs x} to
+can be entered using the X-symbol package.  In \textsc{ascii}, type \isa{abs x} to
 get \isa{\isasymbar x\isasymbar}.
 \end{warn}
 
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/appendix.tex
--- a/doc-src/TutorialI/appendix.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/appendix.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -98,9 +98,9 @@
 \hline
 \end{tabular}
 \end{center}
-\caption{Mathematical symbols, their ASCII-equivalents and X-Symbol codes}
+\caption{Mathematical symbols, their \textsc{ascii}-equivalents and X-symbol codes}
 \label{tab:ascii}
-\end{table}\indexbold{ASCII symbols}
+\end{table}\indexbold{ASCII@\textsc{ascii} symbols}
 
 \input{Misc/document/appendix.tex}
 
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/basics.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -8,12 +8,14 @@
 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
 following the equation
 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
-We assume that the reader is familiar with the basic concepts of both fields.
-For excellent introductions to functional programming consult the textbooks
-by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although
-this tutorial initially concentrates on functional programming, do not be
-misled: HOL can express most mathematical concepts, and functional
-programming is just one particularly simple and ubiquitous instance.
+We do not assume that the reader is familiar with mathematical logic but that
+(s)he is used to logical and set theoretic notation.  In contrast, we do assume
+that the reader is familiar with the basic concepts of functional programming.
+For excellent introductions consult the textbooks by Bird and
+Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although this
+tutorial initially concentrates on functional programming, do not be
+misled: HOL can express most mathematical concepts, and functional programming
+is just one particularly simple and ubiquitous instance.
 
 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.
 This has influenced some of HOL's concrete syntax but is otherwise
@@ -233,7 +235,7 @@
 \end{itemize}
 
 For the sake of readability the usual mathematical symbols are used throughout
-the tutorial. Their ASCII-equivalents are shown in table~\ref{tab:ascii} in
+the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
 the appendix.
 
 
@@ -278,7 +280,7 @@
   General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
 
 Some interfaces (including the shell level) offer special fonts with
-mathematical symbols. For those that do not, remember that ASCII-equivalents
+mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
 are shown in table~\ref{tab:ascii} in the appendix.
 
 Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
@@ -295,7 +297,7 @@
   starts the default logic, which usually is already \texttt{HOL}.  This is
   controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The Isabelle
     System Manual} for more details.} This presents you with Isabelle's most
-basic ASCII interface.  In addition you need to open an editor window to
+basic \textsc{ascii} interface.  In addition you need to open an editor window to
 create theory files.  While you are developing a theory, we recommend to
 type each command into the file first and then enter it into Isabelle by
 copy-and-paste, thus ensuring that you have a complete record of your theory.
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/fp.tex
--- a/doc-src/TutorialI/fp.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -1,16 +1,18 @@
 \chapter{Functional Programming in HOL}
 
 Although on the surface this chapter is mainly concerned with how to write
-functional programs in HOL and how to verify them, most of the
-constructs and proof procedures introduced are general purpose and recur in
-any specification or verification task.
+functional programs in HOL and how to verify them, most of the constructs and
+proof procedures introduced are general purpose and recur in any specification
+or verification task. In fact, it we should really speak of functional
+\emph{modelling} rather than \emph{programming} because our aim is not
+primarily to write programs but to design abstract models of systems.  HOL is
+a specification language that goes well beyond what can be expressed as a
+program. However, for the time being we concentrate on the computable.
 
 The dedicated functional programmer should be warned: HOL offers only
-\emph{total functional programming} --- all functions in HOL must be total;
-lazy data structures are not directly available. On the positive side,
-functions in HOL need not be computable: HOL is a specification language that
-goes well beyond what can be expressed as a program. However, for the time
-being we concentrate on the computable.
+\emph{total functional programming} --- all functions in HOL must be total,
+i.e.\ they must terminate for all inputs; lazy data structures are not
+directly available.
 
 \section{An Introductory Theory}
 \label{sec:intro-theory}
diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Fri Jan 26 15:50:28 2001 +0100
@@ -35,15 +35,12 @@
 Minor fixes in the tutorial
 ===========================
 
-adjust type of ^ in tab:overloading
-
-explanation of term "contrapositive"/contraposition in Rules?
-Index the notion and maybe the rules contrapos_xy
+Adjust FP textbook refs: new Bird, Hudak
+Discrete math textbook: Rosen?
 
-get rid of use_thy in tutorial?
+say something about "abbreviations" when defs are introduced.
 
-Orderings on numbers (with hint that it is overloaded):
-bounded quantifers ALL x<y, <=.
+adjust type of ^ in tab:overloading
 
 an example of induction: !y. A --> B --> C ??
 
@@ -74,16 +71,6 @@
 
 unfold?
 
-Tacticals: , ? +
-Note: + is used in typedef section!
-
-A list of further useful commands (rules? tricks?)
-prefer, defer, print_simpset (-> print_simps?)
-
-demonstrate x : set xs in Sets. Or Tricks chapter?
-
-Appendix with HOL and Isar keywords.
-
 
 Possible exercises
 ==================