Deleted instantiation "set :: (enum) enum"
authorberghofe
Wed, 07 May 2008 10:59:27 +0200
changeset 26815 0cb35f537c91
parent 26814 b3e8d5ec721d
child 26816 e82229ee8f43
Deleted instantiation "set :: (enum) enum"
src/HOL/Library/Enum.thy
--- 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