src/HOL/Library/Executable_Set.thy
changeset 45186 645c6cac779e
parent 45120 717bc892e4d7
child 45231 d85a2fdc586c
     1.1 --- a/src/HOL/Library/Executable_Set.thy	Wed Oct 19 09:11:15 2011 +0200
     1.2 +++ b/src/HOL/Library/Executable_Set.thy	Wed Oct 19 09:11:16 2011 +0200
     1.3 @@ -41,13 +41,6 @@
     1.4  
     1.5  code_datatype Set Coset
     1.6  
     1.7 -consts_code
     1.8 -  Coset ("\<module>Coset")
     1.9 -  Set ("\<module>Set")
    1.10 -attach {*
    1.11 -  datatype 'a set = Set of 'a list | Coset of 'a list;
    1.12 -*} -- {* This assumes that there won't be a @{text Coset} without a @{text Set} *}
    1.13 -
    1.14  
    1.15  subsection {* Basic operations *}
    1.16