pow: unchecked;
authorwenzelm
Sat May 20 23:36:51 2006 +0200 (2006-05-20)
changeset 196846101fbebda1d
parent 19683 3620e494cef2
child 19685 4477003648cc
pow: unchecked;
src/HOL/Algebra/Group.thy
     1.1 --- a/src/HOL/Algebra/Group.thy	Sat May 20 23:36:49 2006 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sat May 20 23:36:51 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 (overloaded)
     1.8 +defs (unchecked 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)