src/HOL/Library/Numeral_Type.thy
changeset 31021 53642251a04f
parent 30960 fec1a04b7220
child 31080 21ffc770ebc0
     1.1 --- a/src/HOL/Library/Numeral_Type.thy	Tue Apr 28 19:15:50 2009 +0200
     1.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Apr 29 14:20:26 2009 +0200
     1.3 @@ -216,12 +216,6 @@
     1.4  apply (simp_all add: Rep_simps zmod_simps ring_simps)
     1.5  done
     1.6  
     1.7 -lemma recpower: "OFCLASS('a, recpower_class)"
     1.8 -apply (intro_classes, unfold definitions)
     1.9 -apply (simp_all add: Rep_simps zmod_simps add_ac mult_assoc
    1.10 -                     mod_pos_pos_trivial size1)
    1.11 -done
    1.12 -
    1.13  end
    1.14  
    1.15  locale mod_ring = mod_type +
    1.16 @@ -340,11 +334,11 @@
    1.17  apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
    1.18  done
    1.19  
    1.20 -instance bit0 :: (finite) "{comm_ring_1,recpower}"
    1.21 -  by (rule bit0.comm_ring_1 bit0.recpower)+
    1.22 +instance bit0 :: (finite) comm_ring_1
    1.23 +  by (rule bit0.comm_ring_1)+
    1.24  
    1.25 -instance bit1 :: (finite) "{comm_ring_1,recpower}"
    1.26 -  by (rule bit1.comm_ring_1 bit1.recpower)+
    1.27 +instance bit1 :: (finite) comm_ring_1
    1.28 +  by (rule bit1.comm_ring_1)+
    1.29  
    1.30  instantiation bit0 and bit1 :: (finite) number_ring
    1.31  begin