author | huffman |
Thu, 18 Jun 2009 18:31:14 -0700 | |
changeset 31717 | d1f7b6245a75 |
parent 31716 | 32f07b47f9c5 |
child 31718 | 7715d4d3586f |
child 31723 | f5cafe803b55 |
--- 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*}