# HG changeset patch
# User paulson
# Date 1086081901 -7200
# Node ID fffab59e0050156271507db40302e1a26f6d32f5
# Parent  0fc75361e0c7cbdbd948208ee4afe08a4fce0dc2
tidied

diff -r 0fc75361e0c7 -r fffab59e0050 src/HOL/Algebra/Group.thy
--- 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