src/ZF/ex/CoUnit.thy

--- a/src/ZF/ex/CoUnit.thy	Mon May 21 14:35:54 2001 +0200
+++ b/src/ZF/ex/CoUnit.thy	Mon May 21 14:36:24 2001 +0200
@@ -19,7 +19,7 @@
 consts
   counit :: i
 codatatype
-  "counit" = Con ("x: counit")
+  "counit" = Con ("x \\<in> counit")
 
 
 (*A similar example, but the constructor is non-degenerate and it works!
@@ -29,6 +29,6 @@
 consts
   counit2 :: i
 codatatype
-  "counit2" = Con2 ("x: counit2", "y: counit2")
+  "counit2" = Con2 ("x \\<in> counit2", "y \\<in> counit2")
 
 end