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