| changeset 16417 | 9bc16273c2d4 |
| parent 14981 | e73f8140af78 |
| child 17274 | 746bb4c56800 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (* Title: HOL/AxClasses/Group.thy |
1 (* Title: HOL/AxClasses/Group.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 theory Group = Main: |
6 theory Group imports Main begin |
7 |
7 |
8 subsection {* Monoids and Groups *} |
8 subsection {* Monoids and Groups *} |
9 |
9 |
10 consts |
10 consts |
11 times :: "'a => 'a => 'a" (infixl "[*]" 70) |
11 times :: "'a => 'a => 'a" (infixl "[*]" 70) |