| changeset 21256 | 47195501ecf7 |
| parent 20432 | 07ec57376051 |
| child 23976 | 9a1859635978 |
--- a/src/HOL/Algebra/Exponent.thy Wed Nov 08 22:24:54 2006 +0100 +++ b/src/HOL/Algebra/Exponent.thy Wed Nov 08 23:11:13 2006 +0100 @@ -5,7 +5,7 @@ exponent p s yields the greatest power of p that divides s. *) -theory Exponent imports Main Primes begin +theory Exponent imports Main Primes Binomial begin section {*The Combinatorial Argument Underlying the First Sylow Theorem*}