1.1 --- a/src/Doc/Logics/document/HOL.tex	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/Doc/Logics/document/HOL.tex	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -1013,22 +1013,22 @@
     1.4          $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
     1.5          & general sum of sets
     1.6  \end{constants}
     1.7 -%\tdx{fst_def}      fst p     == @a. ? b. p = (a,b)
     1.8 -%\tdx{snd_def}      snd p     == @b. ? a. p = (a,b)
     1.9 -%\tdx{split_def}    split c p == c (fst p) (snd p)
    1.10 +%\tdx{fst_def}      fst p         == @a. ? b. p = (a,b)
    1.11 +%\tdx{snd_def}      snd p         == @b. ? a. p = (a,b)
    1.12 +%\tdx{split_def}    case_prod c p == c (fst p) (snd p)
    1.13  \begin{ttbox}\makeatletter
    1.14  \tdx{Sigma_def}    Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
    1.15  
    1.16 -\tdx{Pair_eq}      ((a,b) = (a',b')) = (a=a' & b=b')
    1.17 +\tdx{prod.inject}      ((a,b) = (a',b')) = (a=a' & b=b')
    1.18  \tdx{Pair_inject}  [| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R
    1.19 -\tdx{PairE}        [| !!x y. p = (x,y) ==> Q |] ==> Q
    1.20 +\tdx{prod.exhaust}        [| !!x y. p = (x,y) ==> Q |] ==> Q
    1.21  
    1.22  \tdx{fst_conv}     fst (a,b) = a
    1.23  \tdx{snd_conv}     snd (a,b) = b
    1.24  \tdx{surjective_pairing}  p = (fst p,snd p)
    1.25  
    1.26 -\tdx{split}        split c (a,b) = c a b
    1.27 -\tdx{split_split}  R(split c p) = (! x y. p = (x,y) --> R(c x y))
    1.28 +\tdx{split}        case_prod c (a,b) = c a b
    1.29 +\tdx{prod.split}  R(case_prod c p) = (! x y. p = (x,y) --> R(c x y))
    1.30  
    1.31  \tdx{SigmaI}    [| a:A;  b:B a |] ==> (a,b) : Sigma A B
    1.32  
    1.33 @@ -1059,8 +1059,8 @@
    1.34  \begin{eqnarray*}
    1.35  \hbox{\tt\%($x$,$y$,$z$).\ $t$} 
    1.36     & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\
    1.37 -   & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\
    1.38 -   & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))}
    1.39 +   & \leadsto & \hbox{\tt case_prod(\%$x$.\%($y$,$z$).\ $t$)}\\
    1.40 +   & \leadsto & \hbox{\tt case_prod(\%$x$.\ case_prod(\%$y$ $z$.\ $t$))}
    1.41  \end{eqnarray*}
    1.42  The reverse translation is performed upon printing.
    1.43  \begin{warn}