src/ZF/ex/Data.thy

--- a/src/ZF/ex/Data.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/Data.thy	Mon May 21 14:36:24 2001 +0200
@@ -14,8 +14,8 @@
 
 datatype
   "data(A,B)" = Con0
-              | Con1 ("a: A")
-              | Con2 ("a: A", "b: B")
-              | Con3 ("a: A", "b: B", "d: data(A,B)")
+              | Con1 ("a \\<in> A")
+              | Con2 ("a \\<in> A", "b \\<in> B")
+              | Con3 ("a \\<in> A", "b \\<in> B", "d \\<in> data(A,B)")
 
 end