Deleted instantiation "set :: (type) itself".
authorberghofe
Wed May 07 10:56:50 2008 +0200 (2008-05-07)
changeset 268029eede540a5e8
parent 26801 244184661a09
child 26803 0af0f674845d
Deleted instantiation "set :: (type) itself".
src/HOL/Typedef.thy
     1.1 --- a/src/HOL/Typedef.thy	Wed May 07 10:56:49 2008 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Wed May 07 10:56:50 2008 +0200
     1.3 @@ -160,15 +160,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -instantiation "set" :: ("type") itself
     1.8 -begin
     1.9 -
    1.10 -definition "itself = TYPE('a set)"
    1.11 -
    1.12 -instance ..
    1.13 -
    1.14 -end
    1.15 -
    1.16  hide (open) const itself
    1.17  
    1.18  end