| changeset 16417 | 9bc16273c2d4 |
| parent 14891 | f2e9f7d813af |
| child 19931 | fb32b43e7f80 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
3 |
3 |
4 *) |
4 *) |
5 |
5 |
6 header {* Groups *} |
6 header {* Groups *} |
7 |
7 |
8 theory Group = Main: |
8 theory Group imports Main begin |
9 |
9 |
10 text{*Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and |
10 text{*Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and |
11 Markus Wenzel.*} |
11 Markus Wenzel.*} |
12 |
12 |
13 |
13 |