src/ZF/ex/BT.thy

--- a/src/ZF/ex/BT.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/BT.thy	Mon May 21 14:36:24 2001 +0200
@@ -11,7 +11,7 @@
     bt          :: i=>i
 
 datatype
-  "bt(A)" = Lf  |  Br ("a: A",  "t1: bt(A)",  "t2: bt(A)")
+  "bt(A)" = Lf  |  Br ("a \\<in> A",  "t1: bt(A)",  "t2: bt(A)")
 
 consts
     n_nodes     :: i=>i