src/HOL/Library/Numeral_Type.thy

   Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1
 
 lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)"
 apply (intro_classes, unfold definitions)
 apply (simp_all add: Rep_simps zmod_simps ring_simps)
-done
-
-lemma recpower: "OFCLASS('a, recpower_class)"
-apply (intro_classes, unfold definitions)
-apply (simp_all add: Rep_simps zmod_simps add_ac mult_assoc
-                     mod_pos_pos_trivial size1)
 done
 
 end
 
 locale mod_ring = mod_type +

 apply (rule times_bit1_def [unfolded Abs_bit1'_def])
 apply (rule minus_bit1_def [unfolded Abs_bit1'_def])
 apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
 done
 
-instance bit0 :: (finite) "{comm_ring_1,recpower}"
-  by (rule bit0.comm_ring_1 bit0.recpower)+
-
-instance bit1 :: (finite) "{comm_ring_1,recpower}"
-  by (rule bit1.comm_ring_1 bit1.recpower)+
+instance bit0 :: (finite) comm_ring_1
+  by (rule bit0.comm_ring_1)+
+
+instance bit1 :: (finite) comm_ring_1
+  by (rule bit1.comm_ring_1)+
 
 instantiation bit0 and bit1 :: (finite) number_ring
 begin
 
 definition "(number_of w :: _ bit0) = of_int w"