# HG changeset patch
# User haftmann
# Date 1254846420 -7200
# Node ID 13b153243ed463b93757842179faf514a56d0444
# Parent  b8bee63c72020459289534f01501f542d02e785f
added Coset as constructor

diff -r b8bee63c7202 -r 13b153243ed4 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Tue Oct 06 15:59:12 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Tue Oct 06 18:27:00 2009 +0200
@@ -74,11 +74,12 @@
 types_code
   fset ("(_/ \<module>fset)")
 attach {*
-datatype 'a fset = Set of 'a list;
+datatype 'a fset = Set of 'a list | Coset of 'a list;
 *}
 
 consts_code
   Set ("\<module>Set")
+  Coset ("\<module>Coset")
 
 consts_code
   "empty"             ("{*Fset.empty*}")