# HG changeset patch
# User wenzelm
# Date 1148329758 -7200
# Node ID 1ecda5544e883a54040eff5541e2787741f01d76
# Parent  f48cfaacd92cddc5acc7dcf5ab8fd1b2fa8c7d52
removed unchecked'';

diff -r f48cfaacd92c -r 1ecda5544e88 src/HOL/Algebra/Group.thy
--- 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)