fix name clash with old/new prime libraries
authorhuffman
Thu Jun 18 18:31:14 2009 -0700 (2009-06-18)
changeset 31717d1f7b6245a75
parent 31716 32f07b47f9c5
child 31718 7715d4d3586f
child 31723 f5cafe803b55
fix name clash with old/new prime libraries
src/HOL/Algebra/Exponent.thy
     1.1 --- a/src/HOL/Algebra/Exponent.thy	Thu Jun 18 12:00:03 2009 -0700
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Thu Jun 18 18:31:14 2009 -0700
     1.3 @@ -9,6 +9,8 @@
     1.4  imports Main Primes Binomial
     1.5  begin
     1.6  
     1.7 +hide (open) const GCD.gcd GCD.coprime GCD.prime
     1.8 +
     1.9  section {*Sylow's Theorem*}
    1.10  
    1.11  subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}