author nipkow Fri, 16 Feb 2001 08:27:17 +0100 changeset 11149 e258b536a137 parent 11148 79aa2932b2d7 child 11150 67387142225e
*** empty log message ***
 doc-src/TutorialI/Advanced/Partial.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Advanced/document/Partial.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/CTL/CTL.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/CTL/document/CTL.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/Types/Pairs.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Types/Typedef.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Types/document/Pairs.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/Types/document/Typedef.tex file | annotate | diff | comparison | revisions doc-src/TutorialI/Types/types.tex file | annotate | diff | comparison | revisions
--- 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
*}

--- 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
--- 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
--- 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
--- 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
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 @@

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.
--- 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.
--- 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
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 @@
\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.
--- 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.
--- 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
+\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
-\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}