doc-src/Logics/ZF.tex
changeset 349 0ddc495e8b83
parent 343 8d77f767bd26
child 461 170de0c52a9b
--- a/doc-src/Logics/ZF.tex	Tue May 03 10:40:24 1994 +0200
+++ b/doc-src/Logics/ZF.tex	Tue May 03 10:52:32 1994 +0200
@@ -746,8 +746,8 @@
 \tdx{Pair_inject}     [| <a,b> = <c,d>;  [| a=c; b=d |] ==> P |] ==> P
 \tdx{Pair_neq_0}      <a,b>=0 ==> P
 
-\tdx{fst}             fst(<a,b>) = a
-\tdx{snd}             snd(<a,b>) = b
+\tdx{fst_conv}        fst(<a,b>) = a
+\tdx{snd_conv}        snd(<a,b>) = b
 \tdx{split}           split(\%x y.c(x,y), <a,b>) = c(a,b)
 
 \tdx{SigmaI}          [| a:A;  b:B(a) |] ==> <a,b> : Sigma(A,B)
@@ -1148,7 +1148,7 @@
 \begin{constants} 
   \it symbol  & \it meta-type & \it priority & \it description \\ 
   \sdx{O}       & $[i,i]\To i$  &  Right 60     & composition ($\circ$) \\
-  \cdx{id}      & $\To i$       &       & identity function \\
+  \cdx{id}      & $i\To i$      &       & identity function \\
   \cdx{inj}     & $[i,i]\To i$  &       & injective function space\\
   \cdx{surj}    & $[i,i]\To i$  &       & surjective function space\\
   \cdx{bij}     & $[i,i]\To i$  &       & bijective function space