src/HOL/Algebra/Group.thy
changeset 55415 05f5fdb8d093
parent 47108 2a1953f0d20d
child 55926 3ef14caf5637
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Feb 12 08:35:57 2014 +0100
     1.3 @@ -34,13 +34,13 @@
     1.4  
     1.5  overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
     1.6  begin
     1.7 -  definition "nat_pow G a n = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
     1.8 +  definition "nat_pow G a n = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
     1.9  end
    1.10  
    1.11  overloading int_pow == "pow :: [_, 'a, int] => 'a"
    1.12  begin
    1.13    definition "int_pow G a z =
    1.14 -   (let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
    1.15 +   (let p = rec_nat \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
    1.16      in if z < 0 then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
    1.17  end
    1.18