# HG changeset patch # User berghofe # Date 1210150610 -7200 # Node ID 9eede540a5e86fe5bd652000a7c633c357e853a1 # Parent 244184661a097b3f40cb1be90b79b56b5747d4a8 Deleted instantiation "set :: (type) itself". diff -r 244184661a09 -r 9eede540a5e8 src/HOL/Typedef.thy --- a/src/HOL/Typedef.thy Wed May 07 10:56:49 2008 +0200 +++ b/src/HOL/Typedef.thy Wed May 07 10:56:50 2008 +0200 @@ -160,15 +160,6 @@ end -instantiation "set" :: ("type") itself -begin - -definition "itself = TYPE('a set)" - -instance .. - -end - hide (open) const itself end