--- 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*}
--- 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
--- 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 ***)
--- 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";