--- a/src/HOL/Algebra/Exponent.thy Tue Sep 01 15:39:33 2009 +0200
+++ b/src/HOL/Algebra/Exponent.thy Tue Sep 01 16:00:57 2009 +0200
@@ -1,16 +1,13 @@
(* Title: HOL/Algebra/Exponent.thy
- ID: $Id$
Author: Florian Kammueller, with new proofs by L C Paulson
exponent p s yields the greatest power of p that divides s.
*)
theory Exponent
-imports Main Primes Binomial
+imports Main "~~/src/HOL/Old_Number_Theory/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*}