src/ZF/ex/BT.thy
changeset 753 ec86863e87c8
parent 515 abcc438e7c27
child 935 a94ef3eed456
     1.1 --- a/src/ZF/ex/BT.thy	Mon Nov 28 19:48:30 1994 +0100
     1.2 +++ b/src/ZF/ex/BT.thy	Tue Nov 29 00:31:31 1994 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  datatype
     1.5    "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
     1.6    
     1.7 -rules
     1.8 +defs
     1.9    bt_rec_def
    1.10      "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
    1.11