| changeset 31717 | d1f7b6245a75 |
| parent 30242 | aea5d7fa7ef5 |
| child 31952 | 40501bb2d57c |
--- a/src/HOL/Algebra/Exponent.thy Thu Jun 18 12:00:03 2009 -0700 +++ b/src/HOL/Algebra/Exponent.thy Thu Jun 18 18:31:14 2009 -0700 @@ -9,6 +9,8 @@ imports Main Primes Binomial begin +hide (open) const GCD.gcd GCD.coprime GCD.prime + section {*Sylow's Theorem*} subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}