src/HOL/Algebra/Group.thy
changeset 47108 2a1953f0d20d
parent 46559 69a273fcd53a
child 55415 05f5fdb8d093
     1.1 --- a/src/HOL/Algebra/Group.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -30,7 +30,7 @@
     1.4    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>)}"
     1.5  
     1.6  consts
     1.7 -  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::number] => 'a"  (infixr "'(^')\<index>" 75)
     1.8 +  pow :: "[('a, 'm) monoid_scheme, 'a, 'b::semiring_1] => 'a"  (infixr "'(^')\<index>" 75)
     1.9  
    1.10  overloading nat_pow == "pow :: [_, 'a, nat] => 'a"
    1.11  begin