1.1 --- a/doc-src/Logics/Old_HOL.tex	Tue May 03 10:40:24 1994 +0200
     1.2 +++ b/doc-src/Logics/Old_HOL.tex	Tue May 03 10:52:32 1994 +0200
     1.3 @@ -856,8 +856,8 @@
     1.4  
     1.5  
     1.6  \tdx{Pair_inject}  [| <a, b> = <a',b'>;  [| a=a';  b=b' |] ==> R |] ==> R
     1.7 -\tdx{fst}          fst(<a,b>) = a
     1.8 -\tdx{snd}          snd(<a,b>) = b
     1.9 +\tdx{fst_conv}     fst(<a,b>) = a
    1.10 +\tdx{snd_conv}     snd(<a,b>) = b
    1.11  \tdx{split}        split(<a,b>, c) = c(a,b)
    1.12  
    1.13  \tdx{surjective_pairing}  p = <fst(p),snd(p)>