src/HOL/Algebra/Group.thy
changeset 19699 1ecda5544e88
parent 19684 6101fbebda1d
child 19783 82f365a14960
     1.1 --- a/src/HOL/Algebra/Group.thy	Mon May 22 22:29:16 2006 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Mon May 22 22:29:18 2006 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  consts
     1.5    pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
     1.6  
     1.7 -defs (unchecked overloaded)
     1.8 +defs (overloaded)
     1.9    nat_pow_def: "pow G a n == nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
    1.10    int_pow_def: "pow G a z ==
    1.11      let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)