--- a/doc-src/TutorialI/Misc/document/simp.tex Mon Feb 10 09:45:22 2003 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex Mon Feb 10 15:57:46 2003 +0100
@@ -50,7 +50,7 @@
It is inadvisable to toggle the simplification attribute of a
theorem from a parent theory $A$ in a child theory $B$ for good.
The reason is that if some theory $C$ is based both on $B$ and (via a
- differnt path) on $A$, it is not defined what the simplification attribute
+ different path) on $A$, it is not defined what the simplification attribute
of that theorem will be in $C$: it could be either.
\end{warn}%
\end{isamarkuptext}%
--- a/doc-src/TutorialI/Misc/simp.thy Mon Feb 10 09:45:22 2003 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy Mon Feb 10 15:57:46 2003 +0100
@@ -46,7 +46,7 @@
It is inadvisable to toggle the simplification attribute of a
theorem from a parent theory $A$ in a child theory $B$ for good.
The reason is that if some theory $C$ is based both on $B$ and (via a
- differnt path) on $A$, it is not defined what the simplification attribute
+ different path) on $A$, it is not defined what the simplification attribute
of that theorem will be in $C$: it could be either.
\end{warn}
*}
--- a/doc-src/TutorialI/Sets/sets.tex Mon Feb 10 09:45:22 2003 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex Mon Feb 10 15:57:46 2003 +0100
@@ -377,12 +377,12 @@
\isa{\isacharbraceleft x.\ P\ x\isacharbraceright}. The same thing can
happen with quantifiers: \hbox{\isa{All\ P}}\index{*All (constant)}
is
-\isa{{\isasymforall}z.\ P\ x} and
-\hbox{\isa{Ex\ P}}\index{*Ex (constant)} is \isa{\isasymexists z.\ P\ x};
+\isa{{\isasymforall}x.\ P\ x} and
+\hbox{\isa{Ex\ P}}\index{*Ex (constant)} is \isa{\isasymexists x.\ P\ x};
also \isa{Ball\ A\ P}\index{*Ball (constant)} is
-\isa{{\isasymforall}z\isasymin A.\ P\ x} and
+\isa{{\isasymforall}x\isasymin A.\ P\ x} and
\isa{Bex\ A\ P}\index{*Bex (constant)} is
-\isa{\isasymexists z\isasymin A.\ P\ x}. For indexed unions and
+\isa{\isasymexists x\isasymin A.\ P\ x}. For indexed unions and
intersections, you may see the constants
\cdx{UNION} and \cdx{INTER}\@.
The internal constant for $\varepsilon x.P(x)$ is~\cdx{Eps}.
--- a/doc-src/TutorialI/basics.tex Mon Feb 10 09:45:22 2003 +0100
+++ b/doc-src/TutorialI/basics.tex Mon Feb 10 15:57:46 2003 +0100
@@ -90,7 +90,7 @@
as a direct or indirect parent of all your theories.
\end{warn}
There is also a growing Library~\cite{HOL-Library}\index{Library}
-of useful theories that are not part of \isa{Main} but can to be included
+of useful theories that are not part of \isa{Main} but can be included
among the parents of a theory and will then be loaded automatically.%
\index{theories|)}
@@ -161,10 +161,10 @@
\item[\isa{if $b$ then $t@1$ else $t@2$}]\index{*if expressions}
Here $b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
\item[\isa{let $x$ = $t$ in $u$}]\index{*let expressions}
-is equivalent to $u$ where all occurrences of $x$ have been replaced by
+is equivalent to $u$ where all free occurrences of $x$ have been replaced by
$t$. For example,
\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
-by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
+by semicolons: \isa{let $x@1$ = $t@1$;\dots; $x@n$ = $t@n$ in $u$}.
\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
\index{*case expressions}
evaluates to $e@i$ if $e$ is of the form $c@i$.
--- a/doc-src/TutorialI/tutorial.ind Mon Feb 10 09:45:22 2003 +0100
+++ b/doc-src/TutorialI/tutorial.ind Mon Feb 10 15:57:46 2003 +0100
@@ -182,7 +182,7 @@
\item elimination rules, 69--70
\item \isacommand {end} (command), 14
\item \isa {Eps} (constant), 109
- \item equality, 5
+ \item equality, 6
\subitem of functions, \bold{109}
\subitem of records, 161
\subitem of sets, \bold{106}