equal
deleted
inserted
replaced
11 section {* Monoids and Groups *} |
11 section {* Monoids and Groups *} |
12 |
12 |
13 subsection {* Definitions *} |
13 subsection {* Definitions *} |
14 |
14 |
15 text {* |
15 text {* |
16 Definitions follow \cite{Jacobson:1985}. |
16 Definitions follow @{cite "Jacobson:1985"}. |
17 *} |
17 *} |
18 |
18 |
19 record 'a monoid = "'a partial_object" + |
19 record 'a monoid = "'a partial_object" + |
20 mult :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70) |
20 mult :: "['a, 'a] \<Rightarrow> 'a" (infixl "\<otimes>\<index>" 70) |
21 one :: 'a ("\<one>\<index>") |
21 one :: 'a ("\<one>\<index>") |