src/HOL/Typedef.thy
changeset 26802 9eede540a5e8
parent 26151 4a9b8f15ce7f
child 27295 cfe5244301dd
     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