equal
deleted
inserted
replaced
1 (* Title: HOL/ex/MonoidGroup.thy |
1 (* Title: HOL/ex/MonoidGroup.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel |
3 Author: Markus Wenzel |
4 |
|
5 Monoids and Groups as predicates over record schemes. |
|
6 *) |
4 *) |
7 |
5 |
8 header {* Monoids and Groups *} |
6 header {* Monoids and Groups as predicates over record schemes *} |
9 |
7 |
10 theory MonoidGroup imports Main begin |
8 theory MonoidGroup imports Main begin |
11 |
9 |
12 record 'a monoid_sig = |
10 record 'a monoid_sig = |
13 times :: "'a => 'a => 'a" |
11 times :: "'a => 'a => 'a" |