# HG changeset patch
# User nipkow
# Date 982308437 -3600
# Node ID e258b536a137d95368a5a892be39410aa90564eb
# Parent  79aa2932b2d715beaa92da1b51f7ceee5cec3572
*** empty log message ***

diff -r 79aa2932b2d7 -r e258b536a137 doc-src/TutorialI/Advanced/Partial.thy
--- a/doc-src/TutorialI/Advanced/Partial.thy	Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Fri Feb 16 08:27:17 2001 +0100
@@ -69,7 +69,7 @@
 @{prop[display]"find(f,x) = (if f x = x then x else find(f, f x))"}
 This may be viewed as a fixed point finder or as one half of the well known
 \emph{Union-Find} algorithm.
-The snag is that it may not terminate if @{term f} has nontrivial cycles.
+The snag is that it may not terminate if @{term f} has non-trivial cycles.
 Phrased differently, the relation
 *}
 
diff -r 79aa2932b2d7 -r e258b536a137 doc-src/TutorialI/Advanced/document/Partial.tex
--- a/doc-src/TutorialI/Advanced/document/Partial.tex	Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Fri Feb 16 08:27:17 2001 +0100
@@ -74,7 +74,7 @@
 \end{isabelle}
 This may be viewed as a fixed point finder or as one half of the well known
 \emph{Union-Find} algorithm.
-The snag is that it may not terminate if \isa{f} has nontrivial cycles.
+The snag is that it may not terminate if \isa{f} has non-trivial cycles.
 Phrased differently, the relation%
 \end{isamarkuptext}%
 \isacommand{constdefs}\ step{\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}set{\isachardoublequote}\isanewline
diff -r 79aa2932b2d7 -r e258b536a137 doc-src/TutorialI/CTL/CTL.thy
--- a/doc-src/TutorialI/CTL/CTL.thy	Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Fri Feb 16 08:27:17 2001 +0100
@@ -247,7 +247,7 @@
 What is worth noting here is that we have used @{text fast} rather than
 @{text blast}.  The reason is that @{text blast} would fail because it cannot
 cope with @{thm[source]someI2_ex}: unifying its conclusion with the current
-subgoal is nontrivial because of the nested schematic variables. For
+subgoal is non-trivial because of the nested schematic variables. For
 efficiency reasons @{text blast} does not even attempt such unifications.
 Although @{text fast} can in principle cope with complicated unification
 problems, in practice the number of unifiers arising is often prohibitive and
diff -r 79aa2932b2d7 -r e258b536a137 doc-src/TutorialI/CTL/document/CTL.tex
--- a/doc-src/TutorialI/CTL/document/CTL.tex	Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Fri Feb 16 08:27:17 2001 +0100
@@ -206,7 +206,7 @@
 What is worth noting here is that we have used \isa{fast} rather than
 \isa{blast}.  The reason is that \isa{blast} would fail because it cannot
 cope with \isa{someI{\isadigit{2}}{\isacharunderscore}ex}: unifying its conclusion with the current
-subgoal is nontrivial because of the nested schematic variables. For
+subgoal is non-trivial because of the nested schematic variables. For
 efficiency reasons \isa{blast} does not even attempt such unifications.
 Although \isa{fast} can in principle cope with complicated unification
 problems, in practice the number of unifiers arising is often prohibitive and
diff -r 79aa2932b2d7 -r e258b536a137 doc-src/TutorialI/Types/Pairs.thy
--- a/doc-src/TutorialI/Types/Pairs.thy	Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/Types/Pairs.thy	Fri Feb 16 08:27:17 2001 +0100
@@ -5,7 +5,7 @@
 text{*\label{sec:products}
 Pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
 repertoire of operations: pairing and the two projections @{term fst} and
-@{term snd}. In any nontrivial application of pairs you will find that this
+@{term snd}. In any non-trivial application of pairs you will find that this
 quickly leads to unreadable formulae involvings nests of projections. This
 section is concerned with introducing some syntactic sugar to overcome this
 problem: pattern matching with tuples.
@@ -26,9 +26,6 @@
 @{text"{(x,y,z). x=z}"}\\
 @{term"\<Union>(x,y)\<in>A. {x+y}"}
 \end{quote}
-*}
-
-text{*
 The intuitive meanings of these expressions should be obvious.
 Unfortunately, we need to know in more detail what the notation really stands
 for once we have to reason about it.  Abstraction
@@ -62,7 +59,7 @@
 by(simp add:split_def)
 
 text{* This works well if rewriting with @{thm[source]split_def} finishes the
-proof, as it does above.  But if it doesn't, you end up with exactly what
+proof, as it does above.  But if it does not, you end up with exactly what
 we are trying to avoid: nests of @{term fst} and @{term snd}. Thus this
 approach is neither elegant nor very practical in large examples, although it
 can be effective in small ones.
diff -r 79aa2932b2d7 -r e258b536a137 doc-src/TutorialI/Types/Typedef.thy
--- a/doc-src/TutorialI/Types/Typedef.thy	Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/Types/Typedef.thy	Fri Feb 16 08:27:17 2001 +0100
@@ -265,7 +265,7 @@
 Although @{typ three} could be defined in one line, we have chosen this
 example to demonstrate \isacommand{typedef} because its simplicity makes the
 key concepts particularly easy to grasp. If you would like to see a
-nontrivial example that cannot be defined more directly, we recommend the
+non-trivial example that cannot be defined more directly, we recommend the
 definition of \emph{finite multisets} in the HOL Library.
 
 Let us conclude by summarizing the above procedure for defining a new type.
diff -r 79aa2932b2d7 -r e258b536a137 doc-src/TutorialI/Types/document/Pairs.tex
--- a/doc-src/TutorialI/Types/document/Pairs.tex	Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex	Fri Feb 16 08:27:17 2001 +0100
@@ -9,7 +9,7 @@
 \label{sec:products}
 Pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
 repertoire of operations: pairing and the two projections \isa{fst} and
-\isa{snd}. In any nontrivial application of pairs you will find that this
+\isa{snd}. In any non-trivial application of pairs you will find that this
 quickly leads to unreadable formulae involvings nests of projections. This
 section is concerned with introducing some syntactic sugar to overcome this
 problem: pattern matching with tuples.%
@@ -30,10 +30,7 @@
 \isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}A{\isachardot}\ x{\isacharequal}y}\\
 \isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}\ x{\isacharequal}z{\isacharbraceright}}\\
 \isa{{\isasymUnion}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A{\isachardot}\ {\isacharbraceleft}x\ {\isacharplus}\ y{\isacharbraceright}}
-\end{quote}%
-\end{isamarkuptext}%
-%
-\begin{isamarkuptext}%
+\end{quote}
 The intuitive meanings of these expressions should be obvious.
 Unfortunately, we need to know in more detail what the notation really stands
 for once we have to reason about it.  Abstraction
@@ -66,7 +63,7 @@
 \isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}split{\isacharunderscore}def{\isacharparenright}%
 \begin{isamarkuptext}%
 This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the
-proof, as it does above.  But if it doesn't, you end up with exactly what
+proof, as it does above.  But if it does not, you end up with exactly what
 we are trying to avoid: nests of \isa{fst} and \isa{snd}. Thus this
 approach is neither elegant nor very practical in large examples, although it
 can be effective in small ones.
diff -r 79aa2932b2d7 -r e258b536a137 doc-src/TutorialI/Types/document/Typedef.tex
--- a/doc-src/TutorialI/Types/document/Typedef.tex	Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Typedef.tex	Fri Feb 16 08:27:17 2001 +0100
@@ -262,7 +262,7 @@
 Although \isa{three} could be defined in one line, we have chosen this
 example to demonstrate \isacommand{typedef} because its simplicity makes the
 key concepts particularly easy to grasp. If you would like to see a
-nontrivial example that cannot be defined more directly, we recommend the
+non-trivial example that cannot be defined more directly, we recommend the
 definition of \emph{finite multisets} in the HOL Library.
 
 Let us conclude by summarizing the above procedure for defining a new type.
diff -r 79aa2932b2d7 -r e258b536a137 doc-src/TutorialI/Types/types.tex
--- a/doc-src/TutorialI/Types/types.tex	Fri Feb 16 08:10:28 2001 +0100
+++ b/doc-src/TutorialI/Types/types.tex	Fri Feb 16 08:27:17 2001 +0100
@@ -9,13 +9,18 @@
 \item More about basic types: numbers ({\S}\ref{sec:numbers}), pairs
   ({\S}\ref{sec:products}) and records ({\S}\ref{sec:records}), and how to
   reason about them.
+\item Type classes: how to specify and reason about axiomatic collections of
+  types ({\S}\ref{sec:axclass}).
 \item Introducing your own types: how to introduce new types that
   cannot be constructed with any of the basic methods
   ({\S}\ref{sec:adv-typedef}).
-\item Type classes: how to specify and reason about axiomatic collections of
-  types ({\S}\ref{sec:axclass}).
 \end{itemize}
 
+The material in this section goes beyond the needs of most novices.  Serious
+users should at least skim the sections on basic types and on type classes.
+The latter is fairly advanced: read the beginning to understand what it is
+about, but consult the rest only when necessary.
+
 \section{Numbers}
 \label{sec:numbers}
 
@@ -28,8 +33,6 @@
 \section{Records}
 \label{sec:records}
 
-\input{Types/document/Typedef}
-
 \section{Axiomatic type classes}
 \label{sec:axclass}
 \index{axiomatic type class|(}
@@ -62,3 +65,6 @@
 
 \index{axiomatic type class|)}
 \index{*axclass|)}
+
+
+\input{Types/document/Typedef}