| changeset 31758 | 3edd5f813f01 |
| parent 16417 | 9bc16273c2d4 |
--- a/src/HOL/Isar_examples/Group.thy Mon Jun 22 22:51:08 2009 +0200 +++ b/src/HOL/Isar_examples/Group.thy Mon Jun 22 23:48:24 2009 +0200 @@ -1,11 +1,12 @@ (* Title: HOL/Isar_examples/Group.thy - ID: $Id$ Author: Markus Wenzel, TU Muenchen *) header {* Basic group theory *} -theory Group imports Main begin +theory Group +imports Main +begin subsection {* Groups and calculational reasoning *}