src/HOL/Algebra/Group.thy
changeset 14286 0ae66ffb9784
parent 14254 342634f38451
child 14551 2cb6ff394bfb
     1.1 --- a/src/HOL/Algebra/Group.thy	Wed Dec 10 14:27:50 2003 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Wed Dec 10 14:29:05 2003 +0100
     1.3 @@ -20,8 +20,12 @@
     1.4  
     1.5  subsection {* Definitions *}
     1.6  
     1.7 -record 'a semigroup =
     1.8 +(* Object with a carrier set. *)
     1.9 +
    1.10 +record 'a partial_object =
    1.11    carrier :: "'a set"
    1.12 +
    1.13 +record 'a semigroup = "'a partial_object" +
    1.14    mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70)
    1.15  
    1.16  record 'a monoid = "'a semigroup" +