src/Doc/Logics/document/HOL.tex
 changeset 61424 c3658c18b7bc parent 58318 f95754ca7082 child 64267 b9a1486e79be
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.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.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.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.31  \tdx{SigmaI}    [| a:A;  b:B a |] ==> (a,b) : Sigma A B
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}