# HG changeset patch
# User nipkow
# Date 1044889066 -3600
# Node ID 5402c2eaf393e4c9d7f72bf88c7dcacbe99680dd
# Parent  722593f2f06887bc53d541400a69407107aa5b00
*** empty log message ***

diff -r 722593f2f068 -r 5402c2eaf393 doc-src/TutorialI/Misc/document/simp.tex
--- 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}%
diff -r 722593f2f068 -r 5402c2eaf393 doc-src/TutorialI/Misc/simp.thy
--- 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}
 *} 
diff -r 722593f2f068 -r 5402c2eaf393 doc-src/TutorialI/Sets/sets.tex
--- 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}.
diff -r 722593f2f068 -r 5402c2eaf393 doc-src/TutorialI/basics.tex
--- 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$.
diff -r 722593f2f068 -r 5402c2eaf393 doc-src/TutorialI/tutorial.ind
--- 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}