# HG changeset patch
# User haftmann
# Date 1251813657 -7200
# Node ID 6c19da8e661a09922f7ddb79e1f3b10c665d4a5a
# Parent  521cc9bf2958d6ff60e0bfb62dfcc37ccde63fa6
some reorganization of number theory

diff -r 521cc9bf2958 -r 6c19da8e661a src/HOL/Algebra/Exponent.thy
--- 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*}
diff -r 521cc9bf2958 -r 6c19da8e661a src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Tue Sep 01 15:39:33 2009 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Tue Sep 01 16:00:57 2009 +0200
@@ -4,7 +4,7 @@
 *)
 
 theory IntRing
-imports QuotRing Lattice Int Primes
+imports QuotRing Lattice Int "~~/src/HOL/Old_Number_Theory/Primes"
 begin
 
 
diff -r 521cc9bf2958 -r 6c19da8e661a src/HOL/Algebra/ROOT.ML
--- a/src/HOL/Algebra/ROOT.ML	Tue Sep 01 15:39:33 2009 +0200
+++ b/src/HOL/Algebra/ROOT.ML	Tue Sep 01 16:00:57 2009 +0200
@@ -5,7 +5,7 @@
 *)
 
 (* Preliminaries from set and number theory *)
-no_document use_thys ["FuncSet", "Primes", "Binomial", "Permutation"];
+no_document use_thys ["FuncSet", "~~/src/HOL/Old_Number_Theory/Primes", "Binomial", "Permutation"];
 
 
 (*** New development, based on explicit structures ***)
diff -r 521cc9bf2958 -r 6c19da8e661a src/HOL/Import/HOL/ROOT.ML
--- a/src/HOL/Import/HOL/ROOT.ML	Tue Sep 01 15:39:33 2009 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML	Tue Sep 01 16:00:57 2009 +0200
@@ -1,8 +1,4 @@
-(*  Title:      HOL/Import/HOL/ROOT.ML
-    ID:         $Id$
-    Author:     Sebastian Skalberg (TU Muenchen)
-*)
 
-use_thy "Primes";
+use_thy "~~/src/HOL/Old_Number_Theory/Primes";
 setmp_noncritical quick_and_dirty true use_thy "HOL4Prob";
 setmp_noncritical quick_and_dirty true use_thy "HOL4";