diff -r b89462f9d5f1 -r ec86863e87c8 src/ZF/ex/BT.thy --- a/src/ZF/ex/BT.thy Mon Nov 28 19:48:30 1994 +0100 +++ b/src/ZF/ex/BT.thy Tue Nov 29 00:31:31 1994 +0100 @@ -18,7 +18,7 @@ datatype "bt(A)" = Lf | Br ("a: A", "t1: bt(A)", "t2: bt(A)") -rules +defs bt_rec_def "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"