changeset 58882 | 6e2010ab8bd9 |
parent 58614 | 7338eb25226c |
child 61797 | 458b4e3720ab |
--- a/src/HOL/Isar_Examples/Group_Notepad.thy Sun Nov 02 17:20:45 2014 +0100 +++ b/src/HOL/Isar_Examples/Group_Notepad.thy Sun Nov 02 17:23:48 2014 +0100 @@ -2,7 +2,7 @@ Author: Makarius *) -header \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close> +section \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close> theory Group_Notepad imports Main