src/HOL/Algebra/Exponent.thy
changeset 14706 71590b7733b7
parent 13870 cf947d1ec5ff
child 14889 d7711d6b9014
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Thu May 06 12:43:00 2004 +0200
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Thu May 06 14:14:18 2004 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/GroupTheory/Exponent
     1.5 +(*  Title:      HOL/Algebra/Exponent.thy
     1.6      ID:         $Id$
     1.7      Author:     Florian Kammueller, with new proofs by L C Paulson
     1.8