src/HOL/Nat.thy

 lemma nat_not_singleton: "(\<forall>x. x = (0::nat)) = False"
   by auto
 
 text {* size of a datatype value *}
 
-class size =
+class size = type +
   fixes size :: "'a \<Rightarrow> nat"
 
 text {* @{typ nat} is a datatype *}
 
 rep_datatype nat

   by auto
 
 
 subsection {* Arithmetic operators *}
 
-class power =
+class power = type +
   fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "\<^loc>^" 80)
 
 text {* arithmetic operators @{text "+ -"} and @{text "*"} *}
 
 instance nat :: "{plus, minus, times}" ..