src/HOL/Algebra/Exponent.thy
changeset 35849 b5522b51cb1e
parent 35848 5443079512ea
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Sun Mar 21 16:51:37 2010 +0100
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Sun Mar 21 17:12:31 2010 +0100
     1.3 @@ -1,7 +1,8 @@
     1.4  (*  Title:      HOL/Algebra/Exponent.thy
     1.5 -    Author:     Florian Kammueller, with new proofs by L C Paulson
     1.6 +    Author:     Florian Kammueller
     1.7 +    Author:     L C Paulson
     1.8  
     1.9 -    exponent p s   yields the greatest power of p that divides s.
    1.10 +exponent p s   yields the greatest power of p that divides s.
    1.11  *)
    1.12  
    1.13  theory Exponent