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