doc-src/IsarAdvanced/Classes/Thy/Classes.thy

       neutral_int_def: "\<one> = (0\<Colon>int)"
 
     instance proof
       fix n :: nat
       show "\<one> \<otimes> n = n"
-	unfolding neutral_nat_def mult_nat_def by simp
+	unfolding neutral_nat_def by simp
     next
       fix k :: int
       show "\<one> \<otimes> k = k"
 	unfolding neutral_int_def mult_int_def by simp
     qed