1.1 --- a/src/HOL/IsaMakefile Tue Sep 01 14:13:34 2009 +0200
1.2 +++ b/src/HOL/IsaMakefile Tue Sep 01 15:39:33 2009 +0200
1.3 @@ -34,8 +34,8 @@
1.4 HOL-Modelcheck \
1.5 HOL-NanoJava \
1.6 HOL-Nominal-Examples \
1.7 - HOL-NewNumberTheory \
1.8 - HOL-NumberTheory \
1.9 + HOL-Number_Theory \
1.10 + HOL-Old_Number_Theory \
1.11 HOL-Prolog \
1.12 HOL-SET-Protocol \
1.13 HOL-SizeChange \
1.14 @@ -282,11 +282,13 @@
1.15 Complex.thy \
1.16 Deriv.thy \
1.17 Fact.thy \
1.18 + GCD.thy \
1.19 Integration.thy \
1.20 Lim.thy \
1.21 Limits.thy \
1.22 Ln.thy \
1.23 Log.thy \
1.24 + Lubs.thy \
1.25 MacLaurin.thy \
1.26 NatTransfer.thy \
1.27 NthRoot.thy \
1.28 @@ -294,9 +296,7 @@
1.29 Series.thy \
1.30 Taylor.thy \
1.31 Transcendental.thy \
1.32 - GCD.thy \
1.33 Parity.thy \
1.34 - Lubs.thy \
1.35 PReal.thy \
1.36 Rational.thy \
1.37 RComplete.thy \
1.38 @@ -330,10 +330,10 @@
1.39 Library/Finite_Cartesian_Product.thy Library/FrechetDeriv.thy \
1.40 Library/Fraction_Field.thy Library/Fundamental_Theorem_Algebra.thy \
1.41 Library/Inner_Product.thy Library/Kleene_Algebra.thy \
1.42 - Library/Lattice_Syntax.thy Library/Legacy_GCD.thy \
1.43 + Library/Lattice_Syntax.thy \
1.44 Library/Library.thy Library/List_Prefix.thy Library/List_Set.thy \
1.45 Library/State_Monad.thy Library/Nat_Int_Bij.thy Library/Multiset.thy \
1.46 - Library/Permutation.thy Library/Primes.thy Library/Pocklington.thy \
1.47 + Library/Permutation.thy \
1.48 Library/Quotient.thy Library/Quicksort.thy Library/Nat_Infinity.thy \
1.49 Library/Word.thy Library/README.html Library/Continuity.thy \
1.50 Library/Order_Relation.thy Library/Nested_Environment.thy \
1.51 @@ -487,38 +487,39 @@
1.52 @cd Import/HOLLight; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL HOLLight
1.53
1.54
1.55 -## HOL-NewNumberTheory
1.56 +## HOL-Number_Theory
1.57
1.58 -HOL-NewNumberTheory: HOL $(LOG)/HOL-NewNumberTheory.gz
1.59 +HOL-Number_Theory: HOL $(LOG)/HOL-Number_Theory.gz
1.60
1.61 -$(LOG)/HOL-NewNumberTheory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
1.62 +$(LOG)/HOL-Number_Theory.gz: $(OUT)/HOL $(ALGEBRA_DEPENDENCIES) \
1.63 Library/Multiset.thy \
1.64 - NewNumberTheory/Binomial.thy \
1.65 - NewNumberTheory/Cong.thy \
1.66 - NewNumberTheory/Fib.thy \
1.67 - NewNumberTheory/MiscAlgebra.thy \
1.68 - NewNumberTheory/Residues.thy \
1.69 - NewNumberTheory/UniqueFactorization.thy \
1.70 - NewNumberTheory/ROOT.ML
1.71 - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NewNumberTheory
1.72 + Number_Theory/Binomial.thy \
1.73 + Number_Theory/Cong.thy \
1.74 + Number_Theory/Fib.thy \
1.75 + Number_Theory/MiscAlgebra.thy \
1.76 + Number_Theory/Number_Theory.thy \
1.77 + Number_Theory/Residues.thy \
1.78 + Number_Theory/UniqueFactorization.thy \
1.79 + Number_Theory/ROOT.ML
1.80 + @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Number_Theory
1.81
1.82
1.83 -## HOL-NumberTheory
1.84 +## HOL-Old_Number_Theory
1.85
1.86 -HOL-NumberTheory: HOL $(LOG)/HOL-NumberTheory.gz
1.87 +HOL-Old_Number_Theory: HOL $(LOG)/HOL-Old_Number_Theory.gz
1.88
1.89 -$(LOG)/HOL-NumberTheory.gz: $(OUT)/HOL Library/Permutation.thy \
1.90 - Library/Primes.thy NumberTheory/Fib.thy \
1.91 - NumberTheory/Factorization.thy NumberTheory/BijectionRel.thy \
1.92 - NumberTheory/Chinese.thy NumberTheory/EulerFermat.thy \
1.93 - NumberTheory/IntFact.thy NumberTheory/IntPrimes.thy \
1.94 - NumberTheory/WilsonBij.thy NumberTheory/WilsonRuss.thy \
1.95 - NumberTheory/Finite2.thy NumberTheory/Int2.thy \
1.96 - NumberTheory/EvenOdd.thy NumberTheory/Residues.thy \
1.97 - NumberTheory/Euler.thy NumberTheory/Gauss.thy \
1.98 - NumberTheory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \
1.99 - NumberTheory/ROOT.ML
1.100 - @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL NumberTheory
1.101 +$(LOG)/HOL-Old_Number_Theory.gz: $(OUT)/HOL Library/Permutation.thy \
1.102 + Old_Number_Theory/Primes.thy Old_Number_Theory/Fib.thy \
1.103 + Old_Number_Theory/Factorization.thy Old_Number_Theory/BijectionRel.thy \
1.104 + Old_Number_Theory/Chinese.thy Old_Number_Theory/EulerFermat.thy \
1.105 + Old_Number_Theory/IntFact.thy Old_Number_Theory/IntPrimes.thy \
1.106 + Old_Number_Theory/WilsonBij.thy Old_Number_Theory/WilsonRuss.thy \
1.107 + Old_Number_Theory/Finite2.thy Old_Number_Theory/Int2.thy \
1.108 + Old_Number_Theory/EvenOdd.thy Old_Number_Theory/Residues.thy \
1.109 + Old_Number_Theory/Euler.thy Old_Number_Theory/Gauss.thy \
1.110 + Old_Number_Theory/Quadratic_Reciprocity.thy Library/Infinite_Set.thy \
1.111 + Old_Number_Theory/Legacy_GCD.thy Old_Number_Theory/Pocklington.thy Old_Number_Theory/ROOT.ML
1.112 + @$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Old_Number_Theory
1.113
1.114
1.115 ## HOL-Hoare
1.116 @@ -573,7 +574,7 @@
1.117 Library/FuncSet.thy \
1.118 Library/Multiset.thy \
1.119 Library/Permutation.thy \
1.120 - Library/Primes.thy \
1.121 + Number_Theory/Primes.thy \
1.122 Algebra/AbelCoset.thy \
1.123 Algebra/Bij.thy \
1.124 Algebra/Congruence.thy \
1.125 @@ -876,7 +877,7 @@
1.126 HOL-ex: HOL $(LOG)/HOL-ex.gz
1.127
1.128 $(LOG)/HOL-ex.gz: $(OUT)/HOL Library/Commutative_Ring.thy \
1.129 - Library/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
1.130 + Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
1.131 ex/Arith_Examples.thy \
1.132 ex/Arithmetic_Series_Complex.thy ex/BT.thy ex/BinEx.thy \
1.133 ex/Binary.thy ex/CTL.thy ex/Chinese.thy ex/Classical.thy \