| changeset 65449 | c82e63b11b8b |
| parent 61798 | 27f3c10b0b50 |
| child 67443 | 3abf6a722518 |
| 65448:9bc3b57c1fa7 | 65449:c82e63b11b8b |
|---|---|
1 (* Title: ZF/ex/Group.thy *) |
1 (* Title: ZF/ex/Group.thy *) |
2 |
2 |
3 section \<open>Groups\<close> |
3 section \<open>Groups\<close> |
4 |
4 |
5 theory Group imports Main begin |
5 theory Group imports ZF begin |
6 |
6 |
7 text\<open>Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and |
7 text\<open>Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and |
8 Markus Wenzel.\<close> |
8 Markus Wenzel.\<close> |
9 |
9 |
10 |
10 |