1.1 --- a/doc-src/ZF/ZF.tex	Wed Feb 16 10:50:57 2000 +0100
     1.2 +++ b/doc-src/ZF/ZF.tex	Wed Feb 16 10:51:23 2000 +0100
     1.3 @@ -909,14 +909,14 @@
     1.4  
     1.5  \begin{figure}
     1.6  \begin{ttbox}
     1.7 -\tdx{lamI}         a:A ==> <a,b(a)> : (lam x:A. b(x))
     1.8 -\tdx{lamE}         [| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P 
     1.9 -             |] ==>  P
    1.10 -
    1.11 -\tdx{lam_type}     [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)
    1.12 -
    1.13 -\tdx{beta}         a : A ==> (lam x:A. b(x)) ` a = b(a)
    1.14 -\tdx{eta}          f : Pi(A,B) ==> (lam x:A. f`x) = f
    1.15 +\tdx{lamI}      a:A ==> <a,b(a)> : (lam x:A. b(x))
    1.16 +\tdx{lamE}      [| p: (lam x:A. b(x));  !!x.[| x:A; p=<x,b(x)> |] ==> P 
    1.17 +          |] ==>  P
    1.18 +
    1.19 +\tdx{lam_type}  [| !!x. x:A ==> b(x): B(x) |] ==> (lam x:A. b(x)) : Pi(A,B)
    1.20 +
    1.21 +\tdx{beta}      a : A ==> (lam x:A. b(x)) ` a = b(a)
    1.22 +\tdx{eta}       f : Pi(A,B) ==> (lam x:A. f`x) = f
    1.23  \end{ttbox}
    1.24  \caption{$\lambda$-abstraction} \label{zf-lam}
    1.25  \end{figure}
    1.26 @@ -1263,7 +1263,8 @@
    1.27  \tdx{nat_def}  nat == lfp(lam r: Pow(Inf). {\ttlbrace}0{\ttrbrace} Un {\ttlbrace}succ(x). x:r{\ttrbrace}
    1.28  
    1.29  \tdx{mod_def}  m mod n == transrec(m, \%j f. if j:n then j else f`(j#-n))
    1.30 -\tdx{div_def}  m div n == transrec(m, \%j f. if j:n then 0 else succ(f`(j#-n)))
    1.31 +\tdx{div_def}  m div n == transrec(m, \%j f. if j:n then 0 
    1.32 +                                       else succ(f`(j#-n)))
    1.33  
    1.34  \tdx{nat_case_def}  nat_case(a,b,k) == 
    1.35                THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))
    1.36 @@ -1285,7 +1286,8 @@
    1.37  \tdx{mult_0}        0 #* n = 0
    1.38  \tdx{mult_succ}     succ(m) #* n = n #+ (m #* n)
    1.39  \tdx{mult_commute}  [| m:nat; n:nat |] ==> m #* n = n #* m
    1.40 -\tdx{add_mult_dist} [| m:nat; k:nat |] ==> (m #+ n) #* k = (m #* k){\thinspace}#+{\thinspace}(n #* k)
    1.41 +\tdx{add_mult_dist} [| m:nat; k:nat |] ==> 
    1.42 +              (m #+ n) #* k = (m #* k) #+ (n #* k)
    1.43  \tdx{mult_assoc}
    1.44      [| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)
    1.45  \tdx{mod_quo_equality}
    1.46 @@ -1452,7 +1454,7 @@
    1.47  essentially type-checking.  Such proofs are built by applying rules such as
    1.48  these:
    1.49  \begin{ttbox}
    1.50 -[| ?P ==> ?a : ?A; ~ ?P ==> ?b : ?A |] ==> (if ?P then ?a else ?b) : ?A
    1.51 +[| ?P ==> ?a: ?A; ~?P ==> ?b: ?A |] ==> (if ?P then ?a else ?b): ?A
    1.52  
    1.53  [| ?m : nat; ?n : nat |] ==> ?m #+ ?n : nat
    1.54  
    1.55 @@ -1625,7 +1627,8 @@
    1.56  and forests:
    1.57  \begin{ttbox}
    1.58  [| x : tree_forest(A);
    1.59 -   !!a f. [| a : A; f : forest(A); P(f) |] ==> P(Tcons(a, f)); P(Fnil);
    1.60 +   !!a f. [| a : A; f : forest(A); P(f) |] ==> P(Tcons(a, f)); 
    1.61 +   P(Fnil);
    1.62     !!f t. [| t : tree(A); P(t); f : forest(A); P(f) |]
    1.63            ==> P(Fcons(t, f)) 
    1.64  |] ==> P(x)
    1.65 @@ -1647,7 +1650,7 @@
    1.66  refers to the monotonic operator, \texttt{list}:
    1.67  \begin{ttbox}
    1.68  [| x : term(A);
    1.69 -   !!a l. [| a : A; l : list(Collect(term(A), P)) |] ==> P(Apply(a, l)) 
    1.70 +   !!a l. [| a: A; l: list(Collect(term(A), P)) |] ==> P(Apply(a, l)) 
    1.71  |] ==> P(x)
    1.72  \end{ttbox}
    1.73  The file \texttt{ex/Term.ML} derives two higher-level induction rules, one of
    1.74 @@ -1797,7 +1800,8 @@
    1.75  {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l}
    1.76  {\out  1. ALL x r. Br(x, Lf, r) ~= Lf}
    1.77  {\out  2. !!a t1 t2.}
    1.78 -{\out        [| a : A; t1 : bt(A); ALL x r. Br(x, t1, r) ~= t1; t2 : bt(A);}
    1.79 +{\out        [| a : A; t1 : bt(A);}
    1.80 +{\out           ALL x r. Br(x, t1, r) ~= t1; t2 : bt(A);}
    1.81  {\out           ALL x r. Br(x, t2, r) ~= t2 |]}
    1.82  {\out        ==> ALL x r. Br(x, Br(a, t1, t2), r) ~= Br(a, t1, t2)}
    1.83  \end{ttbox}
    1.84 @@ -1820,7 +1824,8 @@
    1.85  theorems for each constructor.  This is trivial, using the function given us
    1.86  for that purpose:
    1.87  \begin{ttbox}
    1.88 -val Br_iff = bt.mk_free "Br(a,l,r)=Br(a',l',r') <-> a=a' & l=l' & r=r'";
    1.89 +val Br_iff = 
    1.90 +    bt.mk_free "Br(a,l,r)=Br(a',l',r') <-> a=a' & l=l' & r=r'";
    1.91  {\out val Br_iff =}
    1.92  {\out   "Br(?a, ?l, ?r) = Br(?a', ?l', ?r') <->}
    1.93  {\out                     ?a = ?a' & ?l = ?l' & ?r = ?r'" : thm}
    1.94 @@ -1834,7 +1839,8 @@
    1.95  val BrE = bt.mk_cases "Br(a,l,r) : bt(A)";
    1.96  {\out val BrE =}
    1.97  {\out   "[| Br(?a, ?l, ?r) : bt(?A);}
    1.98 -{\out       [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |] ==> ?Q" : thm}
    1.99 +{\out       [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |]}
   1.100 +{\out    ==> ?Q" : thm}
   1.101  \end{ttbox}
   1.102  
   1.103  
   1.104 @@ -2021,7 +2027,7 @@
   1.105    type_elims {\it elimination rules for type-checking}
   1.106  \end{ttbox}
   1.107  A coinductive definition is identical, but starts with the keyword
   1.108 -{\tt coinductive}.  
   1.109 +{\tt co\-inductive}.  
   1.110  
   1.111  The {\tt monos}, {\tt con\_defs}, {\tt type\_intrs} and {\tt type\_elims}
   1.112  sections are optional.  If present, each is specified either as a list of
   1.113 @@ -2031,7 +2037,7 @@
   1.114  error messages.  You can then inspect the file on the temporary directory.
   1.115  
   1.116  \begin{description}
   1.117 -\item[\it domain declarations] consist of one or more items of the form
   1.118 +\item[\it domain declarations] are items of the form
   1.119    {\it string\/}~{\tt <=}~{\it string}, associating each recursive set with
   1.120    its domain.  (The domain is some existing set that is large enough to
   1.121    hold the new set being defined.)