src/HOL/Nat.thy
changeset 29608 564ea783ace8
parent 28952 15a4b2cf8c34
child 29652 f4c6e546b7fe
     1.1 --- a/src/HOL/Nat.thy	Wed Jan 21 18:37:44 2009 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Jan 21 23:40:23 2009 +0100
     1.3 @@ -1515,7 +1515,7 @@
     1.4  
     1.5  subsection {* size of a datatype value *}
     1.6  
     1.7 -class size = type +
     1.8 +class size =
     1.9    fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
    1.10  
    1.11  end