# HG changeset patch
# User wenzelm
# Date 1269188915 -3600
# Node ID dd2636f0f608456575f71bbba69c774d9c72e7cc
# Parent  b5522b51cb1ecd19453a5e89f01242a18be9e41b
modernized overloaded definitions;

diff -r b5522b51cb1e -r dd2636f0f608 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sun Mar 21 17:12:31 2010 +0100
+++ b/src/HOL/Algebra/Group.thy	Sun Mar 21 17:28:35 2010 +0100
@@ -30,13 +30,19 @@
   where "Units G = {y. y \<in> carrier G & (\<exists>x \<in> carrier G. x \<otimes>\<^bsub>G\<^esub> y = \<one>\<^bsub>G\<^esub> & y \<otimes>\<^bsub>G\<^esub> x = \<one>\<^bsub>G\<^esub>)}"
 
 consts
-  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a" (infixr "'(^')\<index>" 75)
+  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a"  (infixr "'(^')\<index>" 75)
+
+overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
+begin
+  definition "nat_pow G a n = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a) n"
+end
 
-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)
-    in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z)"
+overloading int_pow == "pow :: [_, 'a, int] => 'a"
+begin
+  definition "int_pow G a z =
+   (let p = nat_rec \<one>\<^bsub>G\<^esub> (%u b. b \<otimes>\<^bsub>G\<^esub> a)
+    in if neg z then inv\<^bsub>G\<^esub> (p (nat (-z))) else p (nat z))"
+end
 
 locale monoid =
   fixes G (structure)