--- a/src/HOL/Algebra/Group.thy Tue Jun 01 00:26:13 2004 +0200
+++ b/src/HOL/Algebra/Group.thy Tue Jun 01 11:25:01 2004 +0200
@@ -28,10 +28,11 @@
one :: 'a ("\<one>\<index>")
constdefs (structure G)
- m_inv :: "_ => 'a => 'a" ("inv\<index> _" [81] 80)
+ m_inv :: "('a, 'b) monoid_scheme => 'a => 'a" ("inv\<index> _" [81] 80)
"inv x == (THE y. y \<in> carrier G & x \<otimes> y = \<one> & y \<otimes> x = \<one>)"
Units :: "_ => 'a set"
+ --{*The set of invertible elements*}
"Units G == {y. y \<in> carrier G & (EX x : carrier G. x \<otimes> y = \<one> & y \<otimes> x = \<one>)}"
consts