src/HOL/Word/WordArith.thy

   apply (intro_classes)
    apply (simp add: word_mult_commute)
   apply (simp add: word_mult_1)
   done
 
-instance word :: (len0) recpower ..
-
 instance word :: (len0) comm_semiring 
   by (intro_classes) (simp add : word_left_distrib)
 
 instance word :: (len0) ab_group_add ..
 
 instance word :: (len0) comm_ring ..
 
 instance word :: (len) comm_semiring_1 
   by (intro_classes) (simp add: lenw1_zero_neq_one)
-
-instance word :: (len) recpower ..
 
 instance word :: (len) comm_ring_1 ..
 
 instance word :: (len0) comm_semiring_0 ..