src/ZF/ZF.thy
changeset 2286 c2f76a5bad65
parent 1478 2b8c2a7547ab
child 2469 b50b8c0eec01
     1.1 --- a/src/ZF/ZF.thy	Mon Dec 02 10:19:52 1996 +0100
     1.2 +++ b/src/ZF/ZF.thy	Mon Dec 02 10:22:41 1996 +0100
     1.3 @@ -128,10 +128,9 @@
     1.4  
     1.5    "<x, y, z>"   == "<x, <y, z>>"
     1.6    "<x, y>"      == "Pair(x, y)"
     1.7 -  "%<x,y,zs>.b"   == "split(%x <y,zs>.b)"
     1.8 -  "%<x,y>.b"      == "split(%x y.b)"
     1.9 -(* The <= direction fails if split has more than one argument because
    1.10 -   ast-matching fails.  Otherwise it would work fine *)
    1.11 +  "%<x,y,zs>.b" == "split(%x <y,zs>.b)"
    1.12 +  "%<x,y>.b"    == "split(%x y.b)"
    1.13 +
    1.14  
    1.15  defs
    1.16