src/HOL/IsaMakefile

   HOL-MetisExamples \
   HOL-MicroJava \
   HOL-Modelcheck \
   HOL-NanoJava \
   HOL-Nominal-Examples \
-  HOL-NewNumberTheory \
-  HOL-NumberTheory \
+  HOL-Number_Theory \
+  HOL-Old_Number_Theory \
   HOL-Prolog \
   HOL-SET-Protocol \
   HOL-SizeChange \
   HOL-Statespace \
   HOL-Subst \

   Archimedean_Field.thy \
   Complex_Main.thy \
   Complex.thy \
   Deriv.thy \
   Fact.thy \
+  GCD.thy \
   Integration.thy \
   Lim.thy \
   Limits.thy \
   Ln.thy \
   Log.thy \
+  Lubs.thy \
   MacLaurin.thy \
   NatTransfer.thy \
   NthRoot.thy \
   SEQ.thy \
   Series.thy \
   Taylor.thy \
   Transcendental.thy \
-  GCD.thy \
   Parity.thy \
-  Lubs.thy \
   PReal.thy \
   Rational.thy \
   RComplete.thy \
   RealDef.thy \
   RealPow.thy \

   Library/Permutations.thy Library/Determinants.thy Library/Bit.thy	\
   Library/Topology_Euclidean_Space.thy					\
   Library/Finite_Cartesian_Product.thy Library/FrechetDeriv.thy		\
   Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy	\
   Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
-  Library/Lattice_Syntax.thy Library/Legacy_GCD.thy			\
+  Library/Lattice_Syntax.thy			\
   Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy	\
   Library/State_Monad.thy Library/Nat_Int_Bij.thy Library/Multiset.thy	\
-  Library/Permutation.thy Library/Primes.thy Library/Pocklington.thy	\
+  Library/Permutation.thy	\
   Library/Quotient.thy Library/Quicksort.thy Library/Nat_Infinity.thy	\
   Library/Word.thy Library/README.html Library/Continuity.thy		\
   Library/Order_Relation.thy Library/Nested_Environment.thy		\
   Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML		\
   Library/Library/document/root.tex Library/Library/document/root.bib	\

   Import/HOLLight/hollight.imp Import/HOLLight/HOLLight.thy		\
   Import/HOLLight/ROOT.ML
 	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
 
 
-## HOL-NewNumberTheory
-
-HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz
-
-$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
+## HOL-Number_Theory
+
+HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
+
+$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
   Library/Multiset.thy \
-  NewNumberTheory/Binomial.thy \
-  NewNumberTheory/Cong.thy \
-  NewNumberTheory/Fib.thy \
-  NewNumberTheory/MiscAlgebra.thy \
-  NewNumberTheory/Residues.thy \
-  NewNumberTheory/UniqueFactorization.thy  \
-  NewNumberTheory/ROOT.ML
-	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NewNumberTheory
-
-
-## HOL-NumberTheory
-
-HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
-
-$(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL Library/Permutation.thy		\
-  Library/Primes.thy NumberTheory/Fib.thy				\
-  NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy		\
-  NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy			\
-  NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy			\
-  NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy		\
-  NumberTheory/Finite2.thy NumberTheory/Int2.thy			\
-  NumberTheory/EvenOdd.thy NumberTheory/Residues.thy			\
-  NumberTheory/Euler.thy NumberTheory/Gauss.thy				\
-  NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
-  NumberTheory/ROOT.ML
-	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NumberTheory
+  Number_Theory/Binomial.thy \
+  Number_Theory/Cong.thy \
+  Number_Theory/Fib.thy \
+  Number_Theory/MiscAlgebra.thy \
+  Number_Theory/Number_Theory.thy \
+  Number_Theory/Residues.thy \
+  Number_Theory/UniqueFactorization.thy  \
+  Number_Theory/ROOT.ML
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory
+
+
+## HOL-Old_Number_Theory
+
+HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz
+
+$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy		\
+  Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy				\
+  Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy		\
+  Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy			\
+  Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy			\
+  Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy		\
+  Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy			\
+  Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy			\
+  Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy				\
+  Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy	\
+  Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy Old_Number_Theory/ROOT.ML
+	@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
 
 
 ## HOL-Hoare
 
 HOL-Hoare: HOL $(LOG)/HOL-Hoare.gz

   Algebra/ROOT.ML \
   Library/Binomial.thy \
   Library/FuncSet.thy \
   Library/Multiset.thy \
   Library/Permutation.thy \
-  Library/Primes.thy \
+  Number_Theory/Primes.thy \
   Algebra/AbelCoset.thy \
   Algebra/Bij.thy \
   Algebra/Congruence.thy \
   Algebra/Coset.thy \
   Algebra/Divisibility.thy \

 ## HOL-ex
 
 HOL-ex: HOL $(LOG)/HOL-ex.gz
 
 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy		\
-  Library/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
+  Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy		\
   ex/Arith_Examples.thy				\
   ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy		\
   ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy		\
   ex/CodegenSML_Test.thy ex/Codegenerator_Candidates.thy				\
   ex/Codegenerator_Pretty.thy ex/Codegenerator_Test.thy \