src/ZF/qpair.thy
changeset 124 858ab9a9b047
parent 120 09287f26bfb8
equal deleted inserted replaced
123:0a2f744e008a 124:858ab9a9b047
     9 
     9 
    10 W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
    10 W. V. Quine, On Ordered Pairs and Relations, in Selected Logic Papers,
    11 1966.
    11 1966.
    12 *)
    12 *)
    13 
    13 
    14 QPair = Sum +
    14 QPair = Sum + "simpdata" +
    15 consts
    15 consts
    16   QPair     :: "[i, i] => i"               	("<(_;/ _)>")
    16   QPair     :: "[i, i] => i"               	("<(_;/ _)>")
    17   qsplit    :: "[[i,i] => i, i] => i"
    17   qsplit    :: "[[i,i] => i, i] => i"
    18   qfsplit   :: "[[i,i] => o, i] => o"
    18   qfsplit   :: "[[i,i] => o, i] => o"
    19   qconverse :: "i => i"
    19   qconverse :: "i => i"