equal
deleted
inserted
replaced
18 together with a binary, closed operation. |
18 together with a binary, closed operation. |
19 *} |
19 *} |
20 |
20 |
21 subsection {* Definitions *} |
21 subsection {* Definitions *} |
22 |
22 |
23 record 'a semigroup = |
23 (* Object with a carrier set. *) |
|
24 |
|
25 record 'a partial_object = |
24 carrier :: "'a set" |
26 carrier :: "'a set" |
|
27 |
|
28 record 'a semigroup = "'a partial_object" + |
25 mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70) |
29 mult :: "['a, 'a] => 'a" (infixl "\<otimes>\<index>" 70) |
26 |
30 |
27 record 'a monoid = "'a semigroup" + |
31 record 'a monoid = "'a semigroup" + |
28 one :: 'a ("\<one>\<index>") |
32 one :: 'a ("\<one>\<index>") |
29 |
33 |