--- 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 \