src/HOL/Algebra/Group.thy
changeset 14852 fffab59e0050
parent 14803 f7557773cc87
child 14963 d584e32f7d46
     1.1 --- a/src/HOL/Algebra/Group.thy	Tue Jun 01 00:26:13 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Group.thy	Tue Jun 01 11:25:01 2004 +0200
     1.3 @@ -28,10 +28,11 @@
     1.4    one :: 'a ("\<one>\<index>")
     1.5  
     1.6  constdefs (structure G)
     1.7 -  m_inv :: "_ => 'a => 'a" ("inv\<index> _" [81] 80)
     1.8 +  m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
     1.9    "inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
    1.10  
    1.11    Units :: "_ => 'a set"
    1.12 +  --{*The set of invertible elements*}
    1.13    "Units G == {y. y \<in> carrier G & (EX x : carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
    1.14  
    1.15  consts