src/HOL/IsaMakefile
changeset 32479 521cc9bf2958
parent 32402 5731300da417
child 32491 d5d8bea0cd94
child 32496 4ab00a2642c3
--- a/src/HOL/IsaMakefile	Tue Sep 01 14:13:34 2009 +0200
+++ b/src/HOL/IsaMakefile	Tue Sep 01 15:39:33 2009 +0200
@@ -34,8 +34,8 @@
   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 \
@@ -282,11 +282,13 @@
   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 \
@@ -294,9 +296,7 @@
   Series.thy \
   Taylor.thy \
   Transcendental.thy \
-  GCD.thy \
   Parity.thy \
-  Lubs.thy \
   PReal.thy \
   Rational.thy \
   RComplete.thy \
@@ -330,10 +330,10 @@
   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		\
@@ -487,38 +487,39 @@
 	@cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
 
 
-## HOL-NewNumberTheory
+## HOL-Number_Theory
 
-HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz
+HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
 
-$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
+$(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
+  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-NumberTheory
+## HOL-Old_Number_Theory
 
-HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
+HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.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
+$(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
@@ -573,7 +574,7 @@
   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 \
@@ -876,7 +877,7 @@
 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		\