tidied
authorpaulson
Tue Jun 01 11:25:01 2004 +0200 (2004-06-01)
changeset 14852fffab59e0050
parent 14851 0fc75361e0c7
child 14853 8d710bece29f
tidied
src/HOL/Algebra/Group.thy
     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