author | berghofe |
Wed, 07 May 2008 10:59:27 +0200 | |
changeset 26815 | 0cb35f537c91 |
parent 26814 | b3e8d5ec721d |
child 26816 | e82229ee8f43 |
--- a/src/HOL/Library/Enum.thy Wed May 07 10:59:24 2008 +0200 +++ b/src/HOL/Library/Enum.thy Wed May 07 10:59:27 2008 +0200 @@ -261,17 +261,6 @@ by (simp add: sublists_powset length_sublists) qed -instantiation set :: (enum) enum -begin - -definition - "enum = map set (sublists enum)" - -instance by default - (simp_all add: enum_set_def enum_all sublists_powset distinct_set_sublists enum_distinct) - -end - instantiation nibble :: enum begin