
diff -r f081757ce757 -r 434b33c5f827 doc-src/Logics/ZF.tex
--- a/doc-src/Logics/ZF.tex	Fri May 09 19:41:17 1997 +0200
+++ b/doc-src/Logics/ZF.tex	Fri May 09 19:41:46 1997 +0200
@@ -19,13 +19,14 @@
 Thus, we may even regard set theory as a computational logic, loosely
 inspired by Martin-L\"of's Type Theory.
 
-Because {\ZF} is an extension of {\FOL}, it provides the same packages, namely
-{\tt hyp_subst_tac}, the simplifier, and the classical reasoner.  The default
-simpset and claset are usually satisfactory.  Named simpsets include
-\ttindexbold{ZF_ss} (basic set theory rules) and \ttindexbold{rank_ss} (for
-proving termination of well-founded recursion).  Named clasets sets include
-\ttindexbold{ZF_cs} (basic set theory) and \ttindexbold{le_cs} (useful for
-reasoning about the relations $<$ and $\le$).
+Because {\ZF} is an extension of {\FOL}, it provides the same
+packages, namely {\tt hyp_subst_tac}, the simplifier, and the
+classical reasoner.  The default simpset and claset are usually
+satisfactory.  Named simpsets include \ttindexbold{ZF_ss} (basic set
+theory rules) and \ttindexbold{rank_ss} (for proving termination of
+well-founded recursion).  Named clasets include \ttindexbold{ZF_cs}
+(basic set theory) and \ttindexbold{le_cs} (useful for reasoning about
+the relations $<$ and $\le$).
 
 {\tt ZF} has a flexible package for handling inductive definitions,
 such as inference systems, and datatype definitions, such as lists and
@@ -110,8 +111,8 @@
   \tt ``        & $[i,i]\To i$  &  Left 90      & image \\
   \tt -``       & $[i,i]\To i$  &  Left 90      & inverse image \\
   \tt `         & $[i,i]\To i$  &  Left 90      & application \\
-  \sdx{Int}     & $[i,i]\To i$  &  Left 70      & intersection ($\inter$) \\
-  \sdx{Un}      & $[i,i]\To i$  &  Left 65      & union ($\union$) \\
+  \sdx{Int}     & $[i,i]\To i$  &  Left 70      & intersection ($\int$) \\
+  \sdx{Un}      & $[i,i]\To i$  &  Left 65      & union ($\un$) \\
   \tt -         & $[i,i]\To i$  &  Left 65      & set difference ($-$) \\[1ex]
   \tt:          & $[i,i]\To o$  &  Left 50      & membership ($\in$) \\
   \tt <=        & $[i,i]\To o$  &  Left 50      & subset ($\subseteq$) 
@@ -146,8 +147,8 @@
 {\ZF} have type~\tydx{i}, which is the type of individuals and has class~{\tt
   term}.  The type of first-order formulae, remember, is~{\tt o}.
 
-Infix operators include binary union and intersection ($A\union B$ and
-$A\inter B$), set difference ($A-B$), and the subset and membership
+Infix operators include binary union and intersection ($A\un B$ and
+$A\int B$), set difference ($A-B$), and the subset and membership
 relations.  Note that $a$\verb|~:|$b$ is translated to $\neg(a\in b)$.  The
 union and intersection operators ($\bigcup A$ and $\bigcap A$) form the
 union or intersection of a set of sets; $\bigcup A$ means the same as
@@ -160,9 +161,9 @@
 \cdx{cons}:
 \begin{eqnarray*}
    A\cup B              & \equiv &       \bigcup({\tt Upair}(A,B)) \\
-   {\tt cons}(a,B)      & \equiv &        {\tt Upair}(a,a) \union B
+   {\tt cons}(a,B)      & \equiv &        {\tt Upair}(a,a) \un B
 \end{eqnarray*}
-The $\{\ldots\}$ notation abbreviates finite sets constructed in the
+The $\{a@1, \ldots\}$ notation abbreviates finite sets constructed in the
 obvious manner using~{\tt cons} and~$\emptyset$ (the empty set):
 \begin{eqnarray*}
  \{a,b,c\} & \equiv & {\tt cons}(a,{\tt cons}(b,{\tt cons}(c,\emptyset)))
@@ -189,7 +190,7 @@
 \begin{tabular}{rrr} 
   \it external          & \it internal  & \it description \\ 
   $a$ \ttilde: $b$      & \ttilde($a$ : $b$)    & \rm negated membership\\
-  \ttlbrace$a@1$, $\ldots$, $a@n$\ttrbrace  &  cons($a@1$,$\cdots$,cons($a@n$,0)) &
+  \ttlbrace$a@1$, $\ldots$, $a@n$\ttrbrace  &  cons($a@1$,$\ldots$,cons($a@n$,0)) &
         \rm finite set \\
   <$a@1$, $\ldots$, $a@{n-1}$, $a@n$> & 
         Pair($a@1$,\ldots,Pair($a@{n-1}$,$a@n$)\ldots) &
@@ -526,12 +527,12 @@
 
 \section{From basic lemmas to function spaces}
 Faced with so many definitions, it is essential to prove lemmas.  Even
-trivial theorems like $A\inter B=B\inter A$ would be difficult to prove
-from the definitions alone.  Isabelle's set theory derives many rules using
-a natural deduction style.  Ideally, a natural deduction rule should
-introduce or eliminate just one operator, but this is not always practical.
-For most operators, we may forget its definition and use its derived rules
-instead.
+trivial theorems like $A \int B = B \int A$ would be difficult to
+prove from the definitions alone.  Isabelle's set theory derives many
+rules using a natural deduction style.  Ideally, a natural deduction
+rule should introduce or eliminate just one operator, but this is not
+always practical.  For most operators, we may forget its definition
+and use its derived rules instead.
 
 \subsection{Fundamental lemmas}
 Figure~\ref{zf-lemmas1} presents the derived rules for the most basic
@@ -811,7 +812,7 @@
 \begin{warn}
   The translation between patterns and {\tt split} is performed automatically
   by the parser and printer.  Thus the internal and external form of a term
-  may differ, whichs affects proofs.  For example the term {\tt
+  may differ, which affects proofs.  For example the term {\tt
     (\%<x,y>.<y,x>)<a,b>} requires the theorem {\tt split} to rewrite to
   {\tt<b,a>}.
 \end{warn}
@@ -1517,8 +1518,8 @@
 \begin{figure}
 \begin{eqnarray*}
   a\in \emptyset        & \bimp &  \bot\\
-  a \in A \union B      & \bimp &  a\in A \disj a\in B\\
-  a \in A \inter B      & \bimp &  a\in A \conj a\in B\\
+  a \in A \un B      & \bimp &  a\in A \disj a\in B\\
+  a \in A \int B      & \bimp &  a\in A \conj a\in B\\
   a \in A-B             & \bimp &  a\in A \conj \neg (a\in B)\\
   \pair{a,b}\in {\tt Sigma}(A,B)
                         & \bimp &  a\in A \conj b\in B(a)\\
@@ -1625,7 +1626,7 @@
 {\out  2. Pow(A Int B) <= Pow(B)}
 {\out  3. Pow(A) Int Pow(B) <= Pow(A Int B)}
 \end{ttbox}
-Subgoal~1 follows by applying the monotonicity of {\tt Pow} to $A\inter
+Subgoal~1 follows by applying the monotonicity of {\tt Pow} to $A\int
 B\subseteq A$; subgoal~2 follows similarly:
 \index{*Int_lower1 theorem}\index{*Int_lower2 theorem}
 \begin{ttbox}
@@ -1675,7 +1676,7 @@
 {\out  1. !!x. [| x <= A; x <= B |] ==> x <= A Int B}
 \end{ttbox}
 The assumptions are that $x$ is a lower bound of both $A$ and~$B$, but
-$A\inter B$ is the greatest lower bound:\index{*Int_greatest theorem}
+$A\int B$ is the greatest lower bound:\index{*Int_greatest theorem}
 \begin{ttbox}
 by (resolve_tac [Int_greatest] 1);
 {\out Level 9}
@@ -1868,7 +1869,7 @@
 {\out (f Un g) ` a = f ` a}
 {\out  1. f Un g : (PROD x:?A. ?B(x))}
 \end{ttbox}
-To construct functions of the form $f\union g$, we apply
+To construct functions of the form $f\un g$, we apply
 \tdx{fun_disjoint_Un}:
 \begin{ttbox}
 by (resolve_tac [fun_disjoint_Un] 1);




