src/HOL/Typedef.thy
changeset 29608 564ea783ace8
parent 29056 dc08e3990c77
child 29797 08ef36ed2f8a
     1.1 --- a/src/HOL/Typedef.thy	Wed Jan 21 18:37:44 2009 +0100
     1.2 +++ b/src/HOL/Typedef.thy	Wed Jan 21 23:40:23 2009 +0100
     1.3 @@ -123,7 +123,7 @@
     1.4  text {* This class is just a workaround for classes without parameters;
     1.5    it shall disappear as soon as possible. *}
     1.6  
     1.7 -class itself = type + 
     1.8 +class itself = 
     1.9    fixes itself :: "'a itself"
    1.10  
    1.11  setup {*