--- a/src/HOL/Library/Numeral_Type.thy Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Wed Apr 29 14:20:26 2009 +0200
@@ -216,12 +216,6 @@
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 +
@@ -340,11 +334,11 @@
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 bit0 :: (finite) comm_ring_1
+ by (rule bit0.comm_ring_1)+
-instance bit1 :: (finite) "{comm_ring_1,recpower}"
- by (rule bit1.comm_ring_1 bit1.recpower)+
+instance bit1 :: (finite) comm_ring_1
+ by (rule bit1.comm_ring_1)+
instantiation bit0 and bit1 :: (finite) number_ring
begin